Theorems · Theorem · Lie groups
Set.isClosed_centralizer
∀ {M : Type u_1} (s : Set M) [inst : Mul M] [inst_1 : TopologicalSpace M] [SeparatelyContinuousMul M] [T2Space M],
IsClosed s.centralizerIn a Hausdorff magma with continuous multiplication, the centralizer of any set is closed.
- Defined in
- Mathlib.Topology.Algebra.Group.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.ofPredproof · cited by 6,101
- Set.rangeproof · cited by 4,705
- IsClosedstatement and proof · cited by 1,639
- T2Spacestatement and proof · cited by 1,351
- SeparatelyContinuousMulstatement and proof · cited by 133
- isClosed_eqproof · cited by 71
- Set.centralizerstatement · cited by 57
- Set.ofPred_forallproof · cited by 48
- continuous_const_mulproof · cited by 47
- continuous_mul_constproof · cited by 30
Cited by4
Results whose statement or proof uses this declaration.
- StarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizerproof · cited by 1
- Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizerproof · cited by 1
- NonUnitalSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizerproof · cited by 1