Documentation Verification Report

Basic

📁 Source: Mathlib/Order/GaloisConnection/Basic.lean

Statistics

Metric	Count
Definitions `liftBoundedOrder`, `liftCompleteLattice`, `liftLattice`, `liftOrderBot`, `liftSemilatticeInf`, `liftSemilatticeSup`, `liftBoundedOrder`, `liftCompleteLattice`, `liftLattice`, `liftOrderTop`, `liftSemilatticeInf`, `liftSemilatticeSup`, `toGaloisCoinsertion`, `toGaloisInsertion`, `giUnbotDBot`, `gci_Ici_sInf`, `gi_sSup_Iic`	17
Theorems `isGLB_of_l_image`, `isLUB_of_l_image`, `u_biSup_l`, `u_biSup_of_lu_eq_self`, `u_iInf_l`, `u_iSup_l`, `u_iSup_of_lu_eq_self`, `u_inf_l`, `u_sInf_l_image`, `u_sSup_l_image`, `u_sup_l`, `bddAbove_l_image`, `bddBelow_u_image`, `compl`, `isGLB_l`, `isGLB_u_image`, `isGreatest_u`, `isLUB_l_image`, `isLUB_u`, `isLeast_l`, `l_iSup`, `l_iSup₂`, `l_sSup`, `l_sup`, `lowerBounds_u_image`, `u_iInf`, `u_iInf₂`, `u_inf`, `u_sInf`, `upperBounds_l_image`, `isGLB_of_u_image`, `isLUB_of_u_image`, `l_biInf_of_ul_eq_self`, `l_biInf_u`, `l_biSup_u`, `l_iInf_of_ul_eq_self`, `l_iInf_u`, `l_iSup_u`, `l_inf_u`, `l_sInf_u_image`, `l_sSup_u_image`, `l_sup_u`, `galoisConnection_mul_div`, `bddAbove_image`, `bddAbove_preimage`, `bddBelow_image`, `bddBelow_preimage`, `to_galoisConnection`, `gc_Ici_sInf`, `gc_sSup_Iic`, `isGLB_image2_of_isGLB_isGLB`, `isGLB_image2_of_isGLB_isLUB`, `isGLB_image2_of_isLUB_isGLB`, `isGLB_image2_of_isLUB_isLUB`, `isLUB_image2_of_isGLB_isGLB`, `isLUB_image2_of_isGLB_isLUB`, `isLUB_image2_of_isLUB_isGLB`, `isLUB_image2_of_isLUB_isLUB`, `sInf_image2_eq_sInf_sInf`, `sInf_image2_eq_sInf_sSup`, `sInf_image2_eq_sSup_sInf`, `sInf_image2_eq_sSup_sSup`, `sSup_image2_eq_sInf_sInf`, `sSup_image2_eq_sInf_sSup`, `sSup_image2_eq_sSup_sInf`, `sSup_image2_eq_sSup_sSup`	66
Total	83

GaloisCoinsertion

Definitions

Name	Category	Theorems
`liftBoundedOrder` 📖	CompOp	—
`liftCompleteLattice` 📖	CompOp	—
`liftLattice` 📖	CompOp	—
`liftOrderBot` 📖	CompOp	—
`liftSemilatticeInf` 📖	CompOp	—
`liftSemilatticeSup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGLB_of_l_image` 📖	—	`IsGLB` `Preorder.toLE` `Set.image`	—	—	`GaloisInsertion.isLUB_of_u_image`
`isLUB_of_l_image` 📖	—	`IsLUB` `Preorder.toLE` `Set.image`	—	—	`GaloisInsertion.isGLB_of_u_image`
`u_biSup_l` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`GaloisInsertion.l_biInf_u`
`u_biSup_of_lu_eq_self` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`GaloisInsertion.l_biInf_of_ul_eq_self`
`u_iInf_l` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`GaloisInsertion.l_iSup_u`
`u_iSup_l` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`GaloisInsertion.l_iInf_u`
`u_iSup_of_lu_eq_self` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`GaloisInsertion.l_iInf_of_ul_eq_self`
`u_inf_l` 📖	mathematical	—	`SemilatticeInf.toMin`	—	`GaloisInsertion.l_sup_u`
`u_sInf_l_image` 📖	mathematical	—	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set.image`	—	`GaloisInsertion.l_sSup_u_image`
`u_sSup_l_image` 📖	mathematical	—	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image`	—	`GaloisInsertion.l_sInf_u_image`
`u_sup_l` 📖	mathematical	—	`SemilatticeSup.toMax`	—	`GaloisInsertion.l_inf_u`

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_l_image` 📖	mathematical	`GaloisConnection`	`BddAbove` `Preorder.toLE` `Set.image`	—	`upperBounds_l_image` `Monotone.map_bddAbove` `monotone_l`
`bddBelow_u_image` 📖	mathematical	`GaloisConnection`	`BddBelow` `Preorder.toLE` `Set.image`	—	`bddAbove_l_image` `dual`
`compl` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	`Compl.compl` `BooleanAlgebra.toCompl`	—	`le_compl_iff_le_compl` `compl_le_iff_compl_le`
`isGLB_l` 📖	mathematical	`GaloisConnection`	`IsGLB` `Preorder.toLE` `setOf`	—	`IsLeast.isGLB` `isLeast_l`
`isGLB_u_image` 📖	mathematical	`GaloisConnection` `IsGLB` `Preorder.toLE`	`Set.image`	—	`isLUB_l_image` `dual`
`isGreatest_u` 📖	mathematical	`GaloisConnection`	`IsGreatest` `Preorder.toLE` `setOf`	—	`isLeast_l` `dual`
`isLUB_l_image` 📖	mathematical	`GaloisConnection` `IsLUB` `Preorder.toLE`	`Set.image`	—	`Monotone.mem_upperBounds_image` `monotone_l` `l_le` `upperBounds_l_image`
`isLUB_u` 📖	mathematical	`GaloisConnection`	`IsLUB` `Preorder.toLE` `setOf`	—	`IsGreatest.isLUB` `isGreatest_u`
`isLeast_l` 📖	mathematical	`GaloisConnection`	`IsLeast` `Preorder.toLE` `setOf`	—	`le_u_l` `l_le`
`l_iSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`IsLUB.iSup_eq` `Set.range_comp` `sSup_range` `isLUB_l_image` `isLUB_sSup`
`l_iSup₂` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`l_iSup`
`l_sSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `Set` `Set.instMembership`	—	`sSup_eq_iSup` `l_iSup`
`l_sup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`SemilatticeSup.toMax`	—	`IsLUB.unique` `isLUB_l_image` `isLUB_pair` `Set.image_pair`
`lowerBounds_u_image` 📖	mathematical	`GaloisConnection`	`lowerBounds` `Preorder.toLE` `Set.image` `Set.preimage`	—	`upperBounds_l_image` `dual`
`u_iInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iInf` `CompleteSemilatticeInf.toInfSet`	—	`l_iSup` `dual`
`u_iInf₂` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iInf` `CompleteSemilatticeInf.toInfSet`	—	`l_iSup₂` `dual`
`u_inf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`SemilatticeInf.toMin`	—	`l_sup` `dual`
`u_sInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `iInf` `Set` `Set.instMembership`	—	`l_sSup` `dual`
`upperBounds_l_image` 📖	mathematical	`GaloisConnection`	`upperBounds` `Preorder.toLE` `Set.image` `Set.preimage`	—	`Set.ext`

GaloisInsertion

Definitions

Name	Category	Theorems
`liftBoundedOrder` 📖	CompOp	—
`liftCompleteLattice` 📖	CompOp	—
`liftLattice` 📖	CompOp	—
`liftOrderTop` 📖	CompOp	—
`liftSemilatticeInf` 📖	CompOp	—
`liftSemilatticeSup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGLB_of_u_image` 📖	—	`IsGLB` `Preorder.toLE` `Set.image`	—	—	`GaloisConnection.l_le` `gc` `Set.mem_image_of_mem` `LE.le.trans` `le_l_u` `GaloisConnection.monotone_l` `Monotone.mem_lowerBounds_image` `GaloisConnection.monotone_u`
`isLUB_of_u_image` 📖	—	`IsLUB` `Preorder.toLE` `Set.image`	—	—	`LE.le.trans` `le_l_u` `GaloisConnection.monotone_l` `gc` `Set.mem_image_of_mem` `GaloisConnection.l_le` `Monotone.mem_upperBounds_image` `GaloisConnection.monotone_u`
`l_biInf_of_ul_eq_self` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iInf_subtype'` `l_iInf_of_ul_eq_self`
`l_biInf_u` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iInf_subtype'` `l_iInf_u`
`l_biSup_u` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_subtype'` `l_iSup_u`
`l_iInf_of_ul_eq_self` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`l_iInf_u`
`l_iInf_u` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`GaloisConnection.u_iInf` `gc` `l_u_eq`
`l_iSup_u` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`GaloisConnection.l_iSup` `gc` `l_u_eq`
`l_inf_u` 📖	mathematical	—	`SemilatticeInf.toMin`	—	`GaloisConnection.u_inf` `gc` `l_u_eq`
`l_sInf_u_image` 📖	mathematical	—	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set.image`	—	`sInf_image` `l_biInf_u` `sInf_eq_iInf`
`l_sSup_u_image` 📖	mathematical	—	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image`	—	`sSup_image` `l_biSup_u` `sSup_eq_iSup`
`l_sup_u` 📖	mathematical	—	`SemilatticeSup.toMax`	—	`GaloisConnection.l_sup` `gc` `l_u_eq`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`galoisConnection_mul_div` 📖	mathematical	—	`GaloisConnection` `instPreorder`	—	—

OrderIso

Definitions

Name	Category	Theorems
`toGaloisCoinsertion` 📖	CompOp	—
`toGaloisInsertion` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_image` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`GaloisConnection.bddAbove_l_image` `to_galoisConnection`
`bddAbove_preimage` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.preimage` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`bddAbove_image` `image_preimage`
`bddBelow_image` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`bddAbove_image`
`bddBelow_preimage` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.preimage` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`bddBelow_image` `image_preimage`
`to_galoisConnection` 📖	mathematical	—	`GaloisConnection` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `symm`	—	`RelIso.rel_symm_apply`

WithBot

Definitions

Name	Category	Theorems
`giUnbotDBot` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`gci_Ici_sInf` 📖	CompOp	—
`gi_sSup_Iic` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc_Ici_sInf` 📖	mathematical	—	`GaloisConnection` `OrderDual` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `OrderDual.instPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `Set.Ici` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `OrderDual.ofDual`	—	`le_sInf_iff`
`gc_sSup_Iic` 📖	mathematical	—	`GaloisConnection` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `CompleteSemilatticeSup.toPartialOrder` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `Set.Iic`	—	`sSup_le_iff`
`isGLB_image2_of_isGLB_isGLB` 📖	mathematical	`GaloisConnection` `Function.swap` `IsGLB` `Preorder.toLE`	`Set.image2`	—	`isLUB_image2_of_isLUB_isLUB` `GaloisConnection.dual`
`isGLB_image2_of_isGLB_isLUB` 📖	mathematical	`GaloisConnection` `Function.swap` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `OrderDual.ofDual` `IsGLB` `Preorder.toLE` `IsLUB`	`Set.image2`	—	`isGLB_image2_of_isGLB_isGLB`
`isGLB_image2_of_isLUB_isGLB` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `Function.swap` `OrderDual.ofDual` `IsLUB` `Preorder.toLE` `IsGLB`	`Set.image2`	—	`isGLB_image2_of_isGLB_isGLB`
`isGLB_image2_of_isLUB_isLUB` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `Function.swap` `OrderDual.ofDual` `IsLUB` `Preorder.toLE`	`IsGLB` `Set.image2`	—	`isGLB_image2_of_isGLB_isGLB`
`isLUB_image2_of_isGLB_isGLB` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `Function.swap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual` `IsGLB` `Preorder.toLE`	`IsLUB` `Set.image2`	—	`isLUB_image2_of_isLUB_isLUB`
`isLUB_image2_of_isGLB_isLUB` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `Function.swap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual` `IsGLB` `Preorder.toLE` `IsLUB`	`Set.image2`	—	`isLUB_image2_of_isLUB_isLUB`
`isLUB_image2_of_isLUB_isGLB` 📖	mathematical	`GaloisConnection` `Function.swap` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual` `IsLUB` `Preorder.toLE` `IsGLB`	`Set.image2`	—	`isLUB_image2_of_isLUB_isLUB`
`isLUB_image2_of_isLUB_isLUB` 📖	mathematical	`GaloisConnection` `Function.swap` `IsLUB` `Preorder.toLE`	`Set.image2`	—	`GaloisConnection.le_iff_le`
`sInf_image2_eq_sInf_sInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap`	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `Set.image2`	—	`IsGLB.sInf_eq` `isGLB_image2_of_isGLB_isGLB` `isGLB_sInf`
`sInf_image2_eq_sInf_sSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `OrderDual.ofDual`	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `Set.image2` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`sInf_image2_eq_sInf_sInf`
`sInf_image2_eq_sSup_sInf` 📖	mathematical	`GaloisConnection` `OrderDual` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `Function.swap` `OrderDual.ofDual`	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `Set.image2` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`sInf_image2_eq_sInf_sInf`
`sInf_image2_eq_sSup_sSup` 📖	mathematical	`GaloisConnection` `OrderDual` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `Function.swap` `OrderDual.ofDual`	`InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `Set.image2` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`sInf_image2_eq_sInf_sInf`
`sSup_image2_eq_sInf_sInf` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image2` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet`	—	`sSup_image2_eq_sSup_sSup`
`sSup_image2_eq_sInf_sSup` 📖	mathematical	`GaloisConnection` `OrderDual` `OrderDual.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image2` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet`	—	`sSup_image2_eq_sSup_sSup`
`sSup_image2_eq_sSup_sInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.toDual`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image2` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet`	—	`sSup_image2_eq_sSup_sSup`
`sSup_image2_eq_sSup_sSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Function.swap`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image2`	—	`IsLUB.sSup_eq` `isLUB_image2_of_isLUB_isLUB` `isLUB_sSup`

---

← Back to Index