Theorems · Theorem · general topology
SetLike.isDiscrete_iff_discreteTopology
∀ {X : Type u_5} [inst : TopologicalSpace X] {S : Type u_6} [inst_1 : SetLike S X] {s : S},
IsDiscrete ↑s ↔ DiscreteTopology ↥s- Defined in
- Mathlib.Topology.Constructions
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceSetLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- SetLike.coestatement and proof · cited by 8,199
- SetLikestatement and proof · cited by 1,084
- DiscreteTopologystatement and proof · cited by 373
- IsDiscretestatement and proof · cited by 86
- IsDiscrete.to_subtypeproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- Int.tendsto_coe_cofiniteproof · cited by 4
- NumberField.Units.isMaxRank_iff_closure_finiteIndexproof · cited by 1
- Int.tendsto_zmultiplesHom_cofiniteproof · cited by 0
- AddSubgroup.tendsto_zmultiples_subtype_cofiniteproof · cited by 0