Discrete

📁 Source: Mathlib/Topology/Instances/Discrete.lean

Statistics

Metric	Count
Definitions	0
Theorems firstCountableTopology, secondCountableTopology_of_countable, bot_topologicalSpace_eq_generateFrom, of_discreteTopology, of_linearLocallyFinite, discreteTopology_iff_orderTopology_of_pred_succ	6
Total	6

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
firstCountableTopology 📖	mathematical	—	FirstCountableTopology	—	nhds_discrete Filter.isCountablyGenerated_pure
secondCountableTopology_of_countable 📖	mathematical	—	SecondCountableTopology	—	TopologicalSpace.secondCountableTopology_of_countable_cover Set.countable_singleton Unique.instSubsingleton isOpen_discrete Set.iUnion_of_singleton

LinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_topologicalSpace_eq_generateFrom 📖	mathematical	—	Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder TopologicalSpace.generateFrom setOf Set Set.Ioi SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iio	—	DiscreteTopology.eq_bot DiscreteTopology.of_predOrder_succOrder OrderTopology.to_orderClosedTopology

OrderTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_discreteTopology 📖	mathematical	—	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	discreteTopology_iff_orderTopology_of_pred_succ
of_linearLocallyFinite 📖	mathematical	—	OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	of_discreteTopology

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology_iff_orderTopology_of_pred_succ 📖	mathematical	—	DiscreteTopology OrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	DiscreteTopology.eq_bot LinearOrder.bot_topologicalSpace_eq_generateFrom DiscreteTopology.of_predOrder_succOrder OrderTopology.to_orderClosedTopology

---

← Back to Index