class HomogeneousSpace (X : Type u_1) [TopologicalSpace X] : Prop

A space is homogeneous if its homeomorphism group acts transitively.

• is_transitive (x y : X) : ∃ (f : X ≃ₜ X), f x = y