LinearUpperLowerSetTopology

Statistics

Metric	Count
Definitions	0
Theorems `instCompletelyNormalSpaceOfIsLowerSet`, `instCompletelyNormalSpaceOfIsUpperSet`, `instCompletelyNormalSpaceProp`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompletelyNormalSpaceOfIsLowerSet` 📖	mathematical	—	`CompletelyNormalSpace`	—	`instCompletelyNormalSpaceOfIsUpperSet` `OrderDual.instIsUpperSet`
`instCompletelyNormalSpaceOfIsUpperSet` 📖	mathematical	—	`CompletelyNormalSpace`	—	`Set.eq_empty_or_nonempty` `nhdsSet_empty` `lt_asymm` `Topology.IsUpperSet.closure_singleton` `Set.disjoint_of_subset` `subset_refl` `Set.instReflSubset` `Set.singleton_subset_iff` `closure_mono`
`instCompletelyNormalSpaceProp` 📖	mathematical	—	`CompletelyNormalSpace` `sierpinskiSpace`	—	`instCompletelyNormalSpaceOfIsUpperSet` `Topology.IsUpperSet.instProp`

---