`BookProof.ReducedEsa.mem_sector_symProj_iff` (hU2 : ∀ x, U (U x) = x) {x : F} : x ∈ sector (symProj U) ↔ U x = x

Initializing...

`BookProof.ReducedEsa.mem_sector_symProj_iff` (hU2 : ∀ x, U (U x) = x) {x : F} : x ∈ sector (symProj U) ↔ U x = x · Prove2Me