Theorems · Theorem · general topology
IsClopen.isOpen
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsOpen s- Defined in
- Mathlib.Topology.Clopen
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- IsOpenstatement · cited by 2,400
- IsClopenstatement and proof · cited by 189
Cited by21
Results whose statement or proof uses this declaration.
- TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompactsproof · cited by 5
- IsPreconnected.subset_isClopenproof · cited by 4
- PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRingproof · cited by 2
- TopologicalSpace.Compacts.isPreconnected_nonempty_subsetsproof · cited by 2
- ContinuousMap.isClopen_setOfPred_mapsToproof · cited by 2
- MDifferentiable.isLocallyConstantproof · cited by 2
- totallySeparatedSpace_of_t0_of_basis_clopenproof · cited by 2
- Valued.isOpen_sphereproof · cited by 2
- Algebra.quasiFiniteAt_iff_isOpen_singleton_fiberproof · cited by 1
- TopologicalSpace.Clopens.isOpenproof · cited by 1
- UniformSpace.hausdorff.isClosedEmbedding_singletonproof · cited by 1