Documentation Verification Report

LowerUpperTopology

📁 Source: Mathlib/Topology/Order/LowerUpperTopology.lean

Statistics

Metric	Count
Definitions `IsLower`, `lowerBasis`, `withLowerHomeomorph`, `IsUpper`, `upperBasis`, `withUpperHomeomorph`, `WithLower`, `instInhabited`, `instLinearOrder`, `instPartialOrder`, `instPreorder`, `instTopologicalSpace`, `ofLower`, `rec`, `toDualHomeomorph`, `toLower`, `WithUpper`, `instInhabited`, `instLinearOrder`, `instPartialOrder`, `instPreorder`, `instTopologicalSpace`, `ofUpper`, `rec`, `toUpper`, `lower`, `upper`	27
Theorems `instIsLower`, `instIsUpper`, `closure_singleton`, `continuous_iff_Ici`, `instClosedIciTopology`, `isClosed_upperClosure`, `isLowerSet_of_isOpen`, `isOpen_iff_generate_Ici_compl`, `isTopologicalBasis`, `isTopologicalBasis_insert_univ_subbasis`, `isTopologicalSpace_basis`, `isUpperSet_of_isClosed`, `t0Space`, `tendsto_nhds_iff_lt`, `tendsto_nhds_iff_not_le`, `toContinuousInf`, `topology_eq`, `topology_eq_lowerTopology`, `closure_singleton`, `continuous_iff_Iic`, `instClosedIicTopology`, `isClosed_lowerClosure`, `isLowerSet_of_isClosed`, `isOpen_iff_generate_Iic_compl`, `isTopologicalBasis`, `isTopologicalBasis_insert_univ_subbasis`, `isTopologicalSpace_basis`, `isUpperSet_of_isOpen`, `t0Space`, `tendsto_nhds_iff_lt`, `tendsto_nhds_iff_not_le`, `toContinuousInf`, `topology_eq`, `topology_eq_upperTopology`, `continuous_toLower`, `instNonempty`, `isOpen_def`, `isOpen_preimage_ofLower`, `ofLower_inj`, `ofLower_le_ofLower`, `ofLower_lt_ofLower`, `ofLower_symm`, `ofLower_toLower`, `toLower_inj`, `toLower_le_toLower`, `toLower_lt_toLower`, `toLower_ofLower`, `toLower_symm`, `continuous_toUpper`, `instNonempty`, `isOpen_def`, `isOpen_preimage_ofUpper`, `ofUpper_inj`, `ofUpper_le_ofUpper`, `ofUpper_lt_ofUpper`, `ofUpper_symm`, `ofUpper_toUpper`, `toUpper_inj`, `toUpper_le_toUpper`, `toUpper_lt_toUpper`, `toUpper_ofUpper`, `toUpper_symm`, `instIsLowerProd`, `instIsLowerWithLower`, `instIsUpperProd`, `instIsUpperWithUpper`, `isLower_orderDual`, `isUpper_orderDual`, `instIsUpperProp`, `continuous`, `continuous`	71
Total	98

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLower` 📖	mathematical	—	`Topology.IsLower` `OrderDual` `instTopologicalSpace` `instPreorder`	—	`Topology.IsUpper.topology_eq_upperTopology`
`instIsUpper` 📖	mathematical	—	`Topology.IsUpper` `OrderDual` `instTopologicalSpace` `instPreorder`	—	`Topology.IsLower.topology_eq_lowerTopology`

Topology

Definitions

Name	Category	Theorems
`IsLower` 📖	CompData	5 math math: `isUpper_orderDual`, `instIsLowerProd`, `OrderDual.instIsLower`, `instIsLowerWithLower`, `isLower_orderDual`
`IsUpper` 📖	CompData	6 math math: `isUpper_orderDual`, `OrderDual.instIsUpper`, `instIsUpperProp`, `instIsUpperWithUpper`, `instIsUpperProd`, `isLower_orderDual`
`WithLower` 📖	CompOp	15 math math: `WithLower.ofLower_symm`, `WithLower.toLower_inj`, `WithLower.isOpen_def`, `WithLower.instNonempty`, `WithLower.ofLower_le_ofLower`, `WithLower.toLower_le_toLower`, `instIsLowerWithLower`, `WithLower.ofLower_inj`, `WithLower.isOpen_preimage_ofLower`, `WithLower.toLower_ofLower`, `WithLower.toLower_lt_toLower`, `WithLower.continuous_toLower`, `WithLower.toLower_symm`, `WithLower.ofLower_lt_ofLower`, `WithLower.ofLower_toLower`
`WithUpper` 📖	CompOp	15 math math: `WithUpper.continuous_toUpper`, `WithUpper.toUpper_ofUpper`, `WithUpper.ofUpper_lt_ofUpper`, `WithUpper.ofUpper_le_ofUpper`, `WithUpper.instNonempty`, `instIsUpperWithUpper`, `WithUpper.isOpen_preimage_ofUpper`, `WithUpper.ofUpper_symm`, `WithUpper.ofUpper_toUpper`, `WithUpper.toUpper_lt_toUpper`, `WithUpper.ofUpper_inj`, `WithUpper.toUpper_inj`, `WithUpper.toUpper_symm`, `WithUpper.isOpen_def`, `WithUpper.toUpper_le_toUpper`
`lower` 📖	CompOp	6 math math: `IsLower.topology_eq_lowerTopology`, `WithLower.isOpen_def`, `scottHausdorff_le_lower`, `IsLower.topology_eq`, `WithLower.isOpen_preimage_ofLower`, `lawson_le_lower`
`upper` 📖	CompOp	5 math math: `IsUpper.topology_eq_upperTopology`, `WithUpper.isOpen_preimage_ofUpper`, `IsScott.scott_eq_upper_of_completeLinearOrder`, `WithUpper.isOpen_def`, `IsUpper.topology_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLowerProd` 📖	mathematical	—	`IsLower` `instTopologicalSpaceProd` `Prod.instPreorder`	—	`le_antisymm` `le_generateFrom` `IsClosed.isOpen_compl` `IsClosed.prod` `isClosed_Ici` `IsLower.instClosedIciTopology` `TopologicalSpace.IsTopologicalBasis.eq_generateFrom` `TopologicalSpace.IsTopologicalBasis.prod` `IsLower.isTopologicalBasis` `TopologicalSpace.le_generateFrom_iff_subset_isOpen` `Set.image2_subset_iff` `coe_upperClosure` `Set.compl_iUnion` `Set.preimage_iInter` `Set.iInter_congr_Prop` `IsOpen.inter` `Set.Finite.isOpen_biInter` `Set.Ici_bot` `Set.prod_univ` `Set.univ_prod`
`instIsLowerWithLower` 📖	mathematical	—	`IsLower` `WithLower` `WithLower.instTopologicalSpace` `WithLower.instPreorder`	—	—
`instIsUpperProd` 📖	mathematical	—	`IsUpper` `instTopologicalSpaceProd` `Prod.instPreorder`	—	`instIsLowerProd` `OrderDual.instIsLower` `IsLower.topology_eq_lowerTopology`
`instIsUpperWithUpper` 📖	mathematical	—	`IsUpper` `WithUpper` `WithUpper.instTopologicalSpace` `WithUpper.instPreorder`	—	—
`isLower_orderDual` 📖	mathematical	—	`IsLower` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instPreorder` `IsUpper`	—	`isUpper_orderDual`
`isUpper_orderDual` 📖	mathematical	—	`IsUpper` `OrderDual` `OrderDual.instTopologicalSpace` `OrderDual.instPreorder` `IsLower`	—	`OrderDual.instIsLower` `OrderDual.instIsUpper`

Topology.IsLower

Definitions

Name	Category	Theorems
`lowerBasis` 📖	CompOp	1 math math: `isTopologicalBasis`
`withLowerHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_singleton` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `Set.Ici`	—	`Set.Subset.antisymm` `closure_minimal` `Eq.ge` `isClosed_Ici` `instClosedIciTopology` `IsUpperSet.Ici_subset` `isUpperSet_of_isClosed` `isClosed_closure` `subset_closure`
`continuous_iff_Ici` 📖	mathematical	—	`Continuous` `IsClosed` `Set.preimage` `Set.Ici`	—	`topology_eq`
`instClosedIciTopology` 📖	mathematical	—	`ClosedIciTopology`	—	`isOpen_compl_iff` `isOpen_iff_generate_Ici_compl`
`isClosed_upperClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `UpperSet` `Preorder.toLE` `UpperSet.instSetLike` `upperClosure`	—	`UpperSet.coe_iInf` `Set.Finite.isClosed_biUnion` `isClosed_Ici` `instClosedIciTopology`
`isLowerSet_of_isOpen` 📖	mathematical	`IsOpen`	`IsLowerSet` `Preorder.toLE`	—	`isOpen_iff_generate_Ici_compl` `IsUpperSet.compl` `isUpperSet_Ici` `isLowerSet_univ` `IsLowerSet.inter` `isLowerSet_sUnion`
`isOpen_iff_generate_Ici_compl` 📖	mathematical	—	`IsOpen` `TopologicalSpace.GenerateOpen` `setOf` `Set` `Compl.compl` `Set.instCompl` `Set.Ici`	—	`topology_eq`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `lowerBasis`	—	`coe_upperClosure` `Set.compl_iUnion` `Set.ext` `Set.Finite.image` `Set.image_subset_iff` `Set.sInter_image` `Set.finite_range` `Set.Finite.to_subtype` `Set.biInter_range` `Set.sInter_eq_iInter` `Subtype.forall'` `Set.subset_def` `TopologicalSpace.isTopologicalBasis_of_subbasis` `topology_eq`
`isTopologicalBasis_insert_univ_subbasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Set` `Set.instInsert` `Set.univ` `setOf` `Compl.compl` `Set.instCompl` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter` `topology_eq` `Topology.lower.eq_1` `Set.compl_Ici` `Set.Iio_inter_Iio`
`isTopologicalSpace_basis` 📖	mathematical	—	`IsOpen` `Set.univ` `Compl.compl` `Set` `Set.instCompl` `Set.Ici` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot`	—	`Set.compl_Ici` `subset_trans` `Set.instIsTransSubset` `Set.singleton_subset_iff` `Set.subset_insert` `Set.sUnion_singleton` `Set.sUnion_eq_univ_iff` `Set.sUnion_eq_compl_sInter_compl` `compl_inj_iff` `le_antisymm` `Set.sInter_image` `Set.subset_insert_iff_of_notMem` `Set.mem_Ici` `sSup_le_iff` `not_lt` `Set.mem_Iio` `TopologicalSpace.IsTopologicalBasis.open_eq_sUnion` `isTopologicalBasis_insert_univ_subbasis` `TopologicalSpace.IsTopologicalBasis.isOpen`
`isUpperSet_of_isClosed` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE`	—	`isLowerSet_compl` `isLowerSet_of_isOpen` `IsClosed.isOpen_compl`
`t0Space` 📖	mathematical	—	`T0Space`	—	`t0Space_iff_inseparable` `Set.Ici_injective` `closure_singleton`
`tendsto_nhds_iff_lt` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`tendsto_nhds_iff_not_le` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Filter.Eventually` `Preorder.toLE`	—	`topology_eq_lowerTopology`
`toContinuousInf` 📖	mathematical	—	`ContinuousInf` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice`	—	`sInfHom.continuous` `Topology.instIsLowerProd`
`topology_eq` 📖	mathematical	—	`Topology.lower`	—	`topology_eq_lowerTopology`
`topology_eq_lowerTopology` 📖	mathematical	—	`Topology.lower`	—	—

Topology.IsUpper

Definitions

Name	Category	Theorems
`upperBasis` 📖	CompOp	1 math math: `isTopologicalBasis`
`withUpperHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_singleton` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `Set.Iic`	—	`Topology.IsLower.closure_singleton` `OrderDual.instIsLower`
`continuous_iff_Iic` 📖	mathematical	—	`Continuous` `IsClosed` `Set.preimage` `Set.Iic`	—	`Topology.IsLower.continuous_iff_Ici` `OrderDual.instIsLower`
`instClosedIicTopology` 📖	mathematical	—	`ClosedIicTopology`	—	`isOpen_compl_iff` `isOpen_iff_generate_Iic_compl`
`isClosed_lowerClosure` 📖	mathematical	—	`IsClosed` `SetLike.coe` `LowerSet` `Preorder.toLE` `LowerSet.instSetLike` `lowerClosure`	—	`Topology.IsLower.isClosed_upperClosure` `OrderDual.instIsLower`
`isLowerSet_of_isClosed` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE`	—	`isUpperSet_compl` `isUpperSet_of_isOpen` `IsClosed.isOpen_compl`
`isOpen_iff_generate_Iic_compl` 📖	mathematical	—	`IsOpen` `TopologicalSpace.GenerateOpen` `setOf` `Set` `Compl.compl` `Set.instCompl` `Set.Iic`	—	`topology_eq`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `upperBasis`	—	`Topology.IsLower.isTopologicalBasis` `OrderDual.instIsLower`
`isTopologicalBasis_insert_univ_subbasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Set` `Set.instInsert` `Set.univ` `setOf` `Compl.compl` `Set.instCompl` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Topology.IsLower.isTopologicalBasis_insert_univ_subbasis` `OrderDual.instIsLower`
`isTopologicalSpace_basis` 📖	mathematical	—	`IsOpen` `Set.univ` `Compl.compl` `Set` `Set.instCompl` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot`	—	`Topology.IsLower.isTopologicalSpace_basis` `OrderDual.instIsLower`
`isUpperSet_of_isOpen` 📖	mathematical	`IsOpen`	`IsUpperSet` `Preorder.toLE`	—	`Topology.IsLower.isLowerSet_of_isOpen` `OrderDual.instIsLower`
`t0Space` 📖	mathematical	—	`T0Space`	—	`Topology.IsLower.t0Space` `OrderDual.instIsLower`
`tendsto_nhds_iff_lt` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Topology.IsLower.tendsto_nhds_iff_lt` `OrderDual.instIsLower`
`tendsto_nhds_iff_not_le` 📖	mathematical	—	`Filter.Tendsto` `nhds` `Filter.Eventually` `Preorder.toLE`	—	`Topology.IsLower.tendsto_nhds_iff_not_le` `OrderDual.instIsLower`
`toContinuousInf` 📖	mathematical	—	`ContinuousSup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice`	—	`sSupHom.continuous` `Topology.instIsUpperProd`
`topology_eq` 📖	mathematical	—	`Topology.upper`	—	`topology_eq_upperTopology`
`topology_eq_upperTopology` 📖	mathematical	—	`Topology.upper`	—	—

Topology.WithLower

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instLinearOrder` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	5 math math: `ofLower_le_ofLower`, `toLower_le_toLower`, `Topology.instIsLowerWithLower`, `toLower_lt_toLower`, `ofLower_lt_ofLower`
`instTopologicalSpace` 📖	CompOp	4 math math: `isOpen_def`, `Topology.instIsLowerWithLower`, `isOpen_preimage_ofLower`, `continuous_toLower`
`ofLower` 📖	CompOp	8 math math: `ofLower_symm`, `ofLower_le_ofLower`, `ofLower_inj`, `isOpen_preimage_ofLower`, `toLower_ofLower`, `toLower_symm`, `ofLower_lt_ofLower`, `ofLower_toLower`
`rec` 📖	CompOp	—
`toDualHomeomorph` 📖	CompOp	—
`toLower` 📖	CompOp	9 math math: `ofLower_symm`, `toLower_inj`, `isOpen_def`, `toLower_le_toLower`, `toLower_ofLower`, `toLower_lt_toLower`, `continuous_toLower`, `toLower_symm`, `ofLower_toLower`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_toLower` 📖	mathematical	—	`Continuous` `Topology.WithLower` `instTopologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower`	—	`continuous_generateFrom_iff` `IsClosed.isOpen_compl` `isClosed_Ici`
`instNonempty` 📖	mathematical	—	`Topology.WithLower`	—	—
`isOpen_def` 📖	mathematical	—	`IsOpen` `Topology.WithLower` `instTopologicalSpace` `Topology.lower` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower`	—	—
`isOpen_preimage_ofLower` 📖	mathematical	—	`IsOpen` `Topology.WithLower` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLower` `Topology.lower`	—	—
`ofLower_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLower`	—	—
`ofLower_le_ofLower` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLower` `instPreorder`	—	—
`ofLower_lt_ofLower` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLower` `instPreorder`	—	—
`ofLower_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithLower` `ofLower` `toLower`	—	—
`ofLower_toLower` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLower` `toLower`	—	—
`toLower_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower`	—	—
`toLower_le_toLower` 📖	mathematical	—	`Topology.WithLower` `Preorder.toLE` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower`	—	—
`toLower_lt_toLower` 📖	mathematical	—	`Topology.WithLower` `Preorder.toLT` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower`	—	—
`toLower_ofLower` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithLower` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLower` `ofLower`	—	—
`toLower_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithLower` `toLower` `ofLower`	—	—

Topology.WithUpper

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instLinearOrder` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	5 math math: `ofUpper_lt_ofUpper`, `ofUpper_le_ofUpper`, `Topology.instIsUpperWithUpper`, `toUpper_lt_toUpper`, `toUpper_le_toUpper`
`instTopologicalSpace` 📖	CompOp	4 math math: `continuous_toUpper`, `Topology.instIsUpperWithUpper`, `isOpen_preimage_ofUpper`, `isOpen_def`
`ofUpper` 📖	CompOp	8 math math: `toUpper_ofUpper`, `ofUpper_lt_ofUpper`, `ofUpper_le_ofUpper`, `isOpen_preimage_ofUpper`, `ofUpper_symm`, `ofUpper_toUpper`, `ofUpper_inj`, `toUpper_symm`
`rec` 📖	CompOp	—
`toUpper` 📖	CompOp	9 math math: `continuous_toUpper`, `toUpper_ofUpper`, `ofUpper_symm`, `ofUpper_toUpper`, `toUpper_lt_toUpper`, `toUpper_inj`, `toUpper_symm`, `isOpen_def`, `toUpper_le_toUpper`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_toUpper` 📖	mathematical	—	`Continuous` `Topology.WithUpper` `instTopologicalSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper`	—	`continuous_generateFrom_iff` `IsClosed.isOpen_compl` `isClosed_Iic`
`instNonempty` 📖	mathematical	—	`Topology.WithUpper`	—	—
`isOpen_def` 📖	mathematical	—	`IsOpen` `Topology.WithUpper` `instTopologicalSpace` `TopologicalSpace.IsOpen` `Topology.upper` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper`	—	—
`isOpen_preimage_ofUpper` 📖	mathematical	—	`IsOpen` `Topology.WithUpper` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpper` `TopologicalSpace.IsOpen` `Topology.upper`	—	—
`ofUpper_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpper`	—	—
`ofUpper_le_ofUpper` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpper` `instPreorder`	—	—
`ofUpper_lt_ofUpper` 📖	mathematical	—	`Preorder.toLT` `DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpper` `instPreorder`	—	—
`ofUpper_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithUpper` `ofUpper` `toUpper`	—	—
`ofUpper_toUpper` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofUpper` `toUpper`	—	—
`toUpper_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper`	—	—
`toUpper_le_toUpper` 📖	mathematical	—	`Topology.WithUpper` `Preorder.toLE` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper`	—	—
`toUpper_lt_toUpper` 📖	mathematical	—	`Topology.WithUpper` `Preorder.toLT` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper`	—	—
`toUpper_ofUpper` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithUpper` `EquivLike.toFunLike` `Equiv.instEquivLike` `toUpper` `ofUpper`	—	—
`toUpper_symm` 📖	mathematical	—	`Equiv.symm` `Topology.WithUpper` `toUpper` `ofUpper`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsUpperProp` 📖	mathematical	—	`Topology.IsUpper` `sierpinskiSpace` `PartialOrder.toPreorder` `Prop.partialOrder`	—	`Topology.upper.eq_1` `sierpinskiSpace.eq_1` `generateFrom_insert_empty` `le_antisymm` `Set.compl_Iic` `Set.Ioi_False` `Set.Ioi_True` `Set.Iic_True` `Set.compl_univ` `Set.Iic_False` `Prop.compl_singleton`

sInfHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `sInfHom` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instFunLike`	—	`Topology.IsLower.continuous_iff_Ici` `Set.Subset.antisymm` `sInf_le` `le_trans` `InfHomClass.toOrderHomClass` `InfTopHomClass.toInfHomClass` `sInfHomClass.toInfTopHomClass` `instSInfHomClass` `LE.le.trans` `Eq.ge` `sInfHomClass.map_sInf` `OrderHomClass.mono` `OrderHom.instOrderHomClass` `isClosed_Ici` `Topology.IsLower.instClosedIciTopology`

sSupHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	—	`Continuous` `DFunLike.coe` `sSupHom` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instFunLike`	—	`sInfHom.continuous` `OrderDual.instIsLower`

---

← Back to Index