Theorems · Theorem · general topology
isClosed_of_closure_subset
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s ⊆ s → IsClosed s- Defined in
- Mathlib.Topology.Closure
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- IsClosedstatement and proof · cited by 1,639
- closurestatement and proof · cited by 1,254
- LE.le.antisymmproof · cited by 507
- subset_closureproof · cited by 309
- isClosed_closureproof · cited by 195
Cited by12
Results whose statement or proof uses this declaration.
- closure_subset_iff_isClosedproof · cited by 11
- isClosed_setOfPred_isCompactOperatorproof · cited by 3
- ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closedproof · cited by 3
- isClosed_of_spaced_outproof · cited by 2
- MonoidHom.isClosed_range_coeproof · cited by 1
- isClosedMap_iff_closure_imageproof · cited by 1
- Function.LeftInverse.isClosed_rangeproof · cited by 1
- AddMonoidHom.isClosed_range_coeproof · cited by 1
- LinearMap.isClosed_range_coeproof · cited by 1
- continuous_iff_image_closure_subset_closure_imageproof · cited by 0
- AddHom.isClosed_range_coeproof · cited by 0
- MulHom.isClosed_range_coeproof · cited by 0