Booleanisation

📁 Source: Mathlib/Order/Booleanisation.lean

Statistics

Metric	Count
Definitions `Booleanisation`, `LE`, `LT`, `comp`, `instBooleanAlgebra`, `instBot`, `instBoundedOrder`, `instCompl`, `instDecidableEq`, `instDistribLattice`, `instInf`, `instLE`, `instLT`, `instPartialOrder`, `instPreorder`, `instSDiff`, `instSemilatticeInf`, `instSemilatticeSup`, `instSup`, `instTop`, `liftLatticeHom`	21
Theorems `comp_bot`, `comp_inf_comp`, `comp_inf_lift`, `comp_le_comp`, `comp_lt_comp`, `comp_sdiff_comp`, `comp_sdiff_lift`, `comp_sup_comp`, `comp_sup_lift`, `compl_comp`, `compl_lift`, `liftLatticeHom_injective`, `lift_bot`, `lift_inf_comp`, `lift_inf_lift`, `lift_le_comp`, `lift_le_lift`, `lift_lt_comp`, `lift_lt_lift`, `lift_sdiff_comp`, `lift_sdiff_lift`, `lift_sup_comp`, `lift_sup_lift`, `not_comp_le_lift`, `not_comp_lt_lift`	25
Total	46

Booleanisation

Definitions

Name	Category	Theorems
`LE` 📖	CompData	—
`LT` 📖	CompData	—
`comp` 📖	CompOp	18 math math: `comp_sdiff_comp`, `comp_bot`, `not_comp_lt_lift`, `lift_sup_comp`, `comp_lt_comp`, `lift_inf_comp`, `compl_comp`, `compl_lift`, `lift_sdiff_comp`, `not_comp_le_lift`, `comp_sup_comp`, `comp_sdiff_lift`, `lift_lt_comp`, `comp_sup_lift`, `comp_inf_comp`, `comp_inf_lift`, `lift_le_comp`, `comp_le_comp`
`instBooleanAlgebra` 📖	CompOp	1 math math: `liftLatticeHom_injective`
`instBot` 📖	CompOp	1 math math: `lift_bot`
`instBoundedOrder` 📖	CompOp	—
`instCompl` 📖	CompOp	2 math math: `compl_comp`, `compl_lift`
`instDecidableEq` 📖	CompOp	—
`instDistribLattice` 📖	CompOp	—
`instInf` 📖	CompOp	4 math math: `lift_inf_comp`, `comp_inf_comp`, `lift_inf_lift`, `comp_inf_lift`
`instLE` 📖	CompOp	4 math math: `lift_le_lift`, `not_comp_le_lift`, `lift_le_comp`, `comp_le_comp`
`instLT` 📖	CompOp	4 math math: `not_comp_lt_lift`, `comp_lt_comp`, `lift_lt_lift`, `lift_lt_comp`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`instSDiff` 📖	CompOp	4 math math: `comp_sdiff_comp`, `lift_sdiff_lift`, `lift_sdiff_comp`, `comp_sdiff_lift`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`instSup` 📖	CompOp	4 math math: `lift_sup_comp`, `comp_sup_comp`, `comp_sup_lift`, `lift_sup_lift`
`instTop` 📖	CompOp	1 math math: `comp_bot`
`liftLatticeHom` 📖	CompOp	1 math math: `liftLatticeHom_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_bot` 📖	mathematical	—	`comp` `Bot.bot` `GeneralizedBooleanAlgebra.toBot` `Top.top` `Booleanisation` `instTop`	—	—
`comp_inf_comp` 📖	mathematical	—	`Booleanisation` `instInf` `comp` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`comp_inf_lift` 📖	mathematical	—	`Booleanisation` `instInf` `comp` `lift` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`comp_le_comp` 📖	mathematical	—	`Booleanisation` `instLE` `comp` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`comp_lt_comp` 📖	mathematical	—	`Booleanisation` `instLT` `comp` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`comp_sdiff_comp` 📖	mathematical	—	`Booleanisation` `instSDiff` `comp` `lift` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`comp_sdiff_lift` 📖	mathematical	—	`Booleanisation` `instSDiff` `comp` `lift` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`comp_sup_comp` 📖	mathematical	—	`Booleanisation` `instSup` `comp` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`comp_sup_lift` 📖	mathematical	—	`Booleanisation` `instSup` `comp` `lift` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`compl_comp` 📖	mathematical	—	`Compl.compl` `Booleanisation` `instCompl` `comp` `lift`	—	—
`compl_lift` 📖	mathematical	—	`Compl.compl` `Booleanisation` `instCompl` `lift` `comp`	—	—
`liftLatticeHom_injective` 📖	mathematical	—	`Booleanisation` `DFunLike.coe` `LatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `LatticeHom.instFunLike` `liftLatticeHom`	—	`Sum.inl_injective`
`lift_bot` 📖	mathematical	—	`lift` `Bot.bot` `GeneralizedBooleanAlgebra.toBot` `Booleanisation` `instBot`	—	—
`lift_inf_comp` 📖	mathematical	—	`Booleanisation` `instInf` `lift` `comp` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`lift_inf_lift` 📖	mathematical	—	`Booleanisation` `instInf` `lift` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`lift_le_comp` 📖	mathematical	—	`Booleanisation` `instLE` `lift` `comp` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot`	—	—
`lift_le_lift` 📖	mathematical	—	`Booleanisation` `instLE` `lift` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`lift_lt_comp` 📖	mathematical	—	`Booleanisation` `instLT` `lift` `comp` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot`	—	—
`lift_lt_lift` 📖	mathematical	—	`Booleanisation` `instLT` `lift` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`lift_sdiff_comp` 📖	mathematical	—	`Booleanisation` `instSDiff` `lift` `comp` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`lift_sdiff_lift` 📖	mathematical	—	`Booleanisation` `instSDiff` `lift` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`lift_sup_comp` 📖	mathematical	—	`Booleanisation` `instSup` `lift` `comp` `GeneralizedBooleanAlgebra.toSDiff`	—	—
`lift_sup_lift` 📖	mathematical	—	`Booleanisation` `instSup` `lift` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	—	—
`not_comp_le_lift` 📖	mathematical	—	`Booleanisation` `instLE` `comp` `lift`	—	—
`not_comp_lt_lift` 📖	mathematical	—	`Booleanisation` `instLT` `comp` `lift`	—	—

(root)

Definitions

Name	Category	Theorems
`Booleanisation` 📖	CompOp	25 math math: `Booleanisation.comp_sdiff_comp`, `Booleanisation.comp_bot`, `Booleanisation.not_comp_lt_lift`, `Booleanisation.lift_sup_comp`, `Booleanisation.comp_lt_comp`, `Booleanisation.lift_sdiff_lift`, `Booleanisation.lift_le_lift`, `Booleanisation.lift_inf_comp`, `Booleanisation.compl_comp`, `Booleanisation.compl_lift`, `Booleanisation.lift_sdiff_comp`, `Booleanisation.liftLatticeHom_injective`, `Booleanisation.not_comp_le_lift`, `Booleanisation.lift_lt_lift`, `Booleanisation.comp_sup_comp`, `Booleanisation.comp_sdiff_lift`, `Booleanisation.lift_lt_comp`, `Booleanisation.comp_sup_lift`, `Booleanisation.comp_inf_comp`, `Booleanisation.lift_inf_lift`, `Booleanisation.comp_inf_lift`, `Booleanisation.lift_sup_lift`, `Booleanisation.lift_le_comp`, `Booleanisation.lift_bot`, `Booleanisation.comp_le_comp`

---

← Back to Index