Lindelof

Statistics

Metric	Count
Definitions	0
Theorems `exists_countable_lowerSemicontinuous_isLUB`, `exists_countable_upperSemicontinuous_isGLB`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_countable_lowerSemicontinuous_isLUB` 📖	mathematical	`LowerSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsLUB` `Pi.hasLe` `Preorder.toLE`	`Set` `Set.instHasSubset` `Set.Countable`	—	`exists_countable_upperSemicontinuous_isGLB` `instOrderClosedTopologyOrderDual` `OrderDual.denselyOrdered` `instSeparableSpaceOrderDual`
`exists_countable_upperSemicontinuous_isGLB` 📖	mathematical	`UpperSemicontinuous` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsGLB` `Pi.hasLe` `Preorder.toLE`	`Set` `Set.instHasSubset` `Set.Countable`	—	`TopologicalSpace.exists_countable_dense` `UpperSemicontinuous.isOpen_preimage` `Set.ext` `isGLB_lt_iff` `Set.image_congr` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `eq_open_union_countable` `Set.image_val_subset` `Set.Countable.image` `Set.biUnion_image` `Set.iUnion₂_subset` `Set.Countable.biUnion` `lowerBounds_mono_set` `Set.image_mono` `Dense.exists_between` `LT.lt.trans` `LE.le.trans_lt` `Set.mem_image_of_mem` `Set.mem_iUnion₂_of_mem`

---