AlexandrovDiscrete

📁 Source: Mathlib/Topology/Separation/AlexandrovDiscrete.lean

Statistics

Metric	Count
Definitions AlexandrovDiscrete	1
Theorems instDiscreteTopologyOfAlexandrovDiscreteOfT1Space, nhdsKer_eq_of_t1Space	2
Total	3

(root)

Definitions

Name	Category	Theorems
AlexandrovDiscrete 📖	CompData	15 math math: DiscreteTopology.toAlexandrovDiscrete, Topology.IsUpperSet.toAlexandrovDiscrete, Sum.instAlexandrovDiscrete, alexandrovDiscrete_iff_isClosed, alexandrovDiscrete_iff, Quotient.instAlexandrovDiscrete, alexandrovDiscrete_coinduced, Topology.IsInducing.alexandrovDiscrete, AlexandrovDiscrete.sup, Finite.toAlexandrovDiscrete, Topology.IsLowerSet.toAlexandrovDiscrete, AlexDisc.is_alexandrovDiscrete, alexandrovDiscrete_iff_nhds, Subtype.instAlexandrovDiscrete, Prod.instAlexandrovDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopologyOfAlexandrovDiscreteOfT1Space 📖	mathematical	—	DiscreteTopology	—	nhdsKer_eq_of_t1Space Filter.principal_singleton
nhdsKer_eq_of_t1Space 📖	mathematical	—	nhdsKer	—	Set.ext specializes_eq_eq

---

← Back to Index