theorem QuotientGroup.indiscreteTopology_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} : IndiscreteTopology (G ⧸ N) ↔ N.topologicalClosure = ⊤

A quotient group has the indiscrete topology if and only if the topological closure of the subgroup is the entire group.

theorem QuotientAddGroup.indiscreteTopology_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {N : AddSubgroup G} : IndiscreteTopology (G ⧸ N) ↔ N.topologicalClosure = ⊤

The quotient by an additive subgroup has the indiscrete topology if and only if the topological closure of the subgroup is the entire group.

theorem QuotientGroup.indiscreteTopology {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} : N.topologicalClosure = ⊤ → IndiscreteTopology (G ⧸ N)

Alias of the reverse direction of QuotientGroup.indiscreteTopology_iff.

---

A quotient group has the indiscrete topology if and only if the topological closure of the subgroup is the entire group.

theorem QuotientAddGroup.indiscreteTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {N : AddSubgroup G} : N.topologicalClosure = ⊤ → IndiscreteTopology (G ⧸ N)

Alias of the reverse direction of QuotientAddGroup.indiscreteTopology_iff.

---

The quotient by an additive subgroup has the indiscrete topology if and only if the topological closure of the subgroup is the entire group.

theorem QuotientGroup.topologicalClosure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [IndiscreteTopology (G ⧸ N)] : N.topologicalClosure = ⊤

theorem QuotientAddGroup.topologicalClosure_eq_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [IndiscreteTopology (G ⧸ N)] : N.topologicalClosure = ⊤

theorem QuotientGroup.nontrivialTopology_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} : NontrivialTopology (G ⧸ N) ↔ N.topologicalClosure ≠ ⊤

A quotient group has a nontrivial topology if and only if the topological closure of the subgroup is not the entire group.

theorem QuotientAddGroup.nontrivialTopology_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {N : AddSubgroup G} : NontrivialTopology (G ⧸ N) ↔ N.topologicalClosure ≠ ⊤

The quotient by an additive subgroup has a nontrivial topology if and only if the topological closure of the subgroup is not the entire group.

theorem QuotientGroup.nontrivialTopology {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} : N.topologicalClosure ≠ ⊤ → NontrivialTopology (G ⧸ N)

Alias of the reverse direction of QuotientGroup.nontrivialTopology_iff.

---

A quotient group has a nontrivial topology if and only if the topological closure of the subgroup is not the entire group.

theorem QuotientAddGroup.nontrivialTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {N : AddSubgroup G} : N.topologicalClosure ≠ ⊤ → NontrivialTopology (G ⧸ N)

Alias of the reverse direction of QuotientAddGroup.nontrivialTopology_iff.

---

The quotient by an additive subgroup has a nontrivial topology if and only if the topological closure of the subgroup is not the entire group.

theorem QuotientGroup.topologicalClosure_ne_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [NontrivialTopology (G ⧸ N)] : N.topologicalClosure ≠ ⊤

theorem QuotientAddGroup.topologicalClosure_ne_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [NontrivialTopology (G ⧸ N)] : N.topologicalClosure ≠ ⊤