Documentation Verification Report

Boundary

📁 Source: Mathlib/Order/Heyting/Boundary.lean

Statistics

Metric	Count
Definitions `boundary`, `«term∂_»`	2
Theorems `boundary_bot`, `boundary_eq_bot`, `boundary_hnot_hnot`, `boundary_hnot_le`, `boundary_idem`, `boundary_inf`, `boundary_inf_le`, `boundary_le`, `boundary_le_boundary_sup_sup_boundary_inf_left`, `boundary_le_boundary_sup_sup_boundary_inf_right`, `boundary_le_hnot`, `boundary_sup_le`, `boundary_sup_sup_boundary_inf`, `boundary_top`, `hnot_boundary`, `hnot_eq_top_iff_exists_boundary`, `hnot_hnot_sup_boundary`, `inf_hnot_self`	18
Total	20

Coheyting

Definitions

Name	Category	Theorems
`boundary` 📖	CompOp	18 math math: `boundary_top`, `boundary_le_hnot`, `hnot_boundary`, `hnot_eq_top_iff_exists_boundary`, `hnot_hnot_sup_boundary`, `boundary_sup_le`, `boundary_inf`, `boundary_hnot_hnot`, `boundary_eq_bot`, `inf_hnot_self`, `boundary_inf_le`, `boundary_hnot_le`, `boundary_le_boundary_sup_sup_boundary_inf_left`, `boundary_le`, `boundary_idem`, `boundary_sup_sup_boundary_inf`, `boundary_bot`, `boundary_le_boundary_sup_sup_boundary_inf_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundary_bot` 📖	mathematical	—	`boundary` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BoundedOrder.toOrderBot` `CoheytingAlgebra.toBoundedOrder`	—	`bot_inf_eq`
`boundary_eq_bot` 📖	mathematical	—	`boundary` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Bot.bot` `BooleanAlgebra.toBot`	—	`inf_compl_eq_bot`
`boundary_hnot_hnot` 📖	mathematical	—	`boundary` `HNot.hnot` `CoheytingAlgebra.toHNot`	—	`hnot_hnot_hnot` `inf_comm`
`boundary_hnot_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `HNot.hnot` `CoheytingAlgebra.toHNot`	—	`Eq.trans_le` `inf_comm` `inf_le_inf_right` `hnot_hnot_le`
`boundary_idem` 📖	mathematical	—	`boundary`	—	`boundary.eq_1` `hnot_boundary` `inf_top_eq`
`boundary_inf` 📖	mathematical	—	`boundary` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`hnot_inf_distrib` `inf_sup_left` `inf_right_comm` `inf_assoc`
`boundary_inf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`Eq.trans_le` `boundary_inf` `sup_le_sup` `inf_le_left` `inf_le_right`
`boundary_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary`	—	`inf_le_left`
`boundary_le_boundary_sup_sup_boundary_inf_left` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin`	—	`sup_inf_left` `sup_comm` `sup_inf_right` `sup_right_idem` `sup_assoc` `le_sup_of_le_left` `inf_le_left` `inf_le_of_right_le` `hnot_le_iff_codisjoint_right` `codisjoint_left_comm` `codisjoint_hnot_left` `le_sup_of_le_right` `Codisjoint.mono_right` `hnot_anti` `codisjoint_hnot_right`
`boundary_le_boundary_sup_sup_boundary_inf_right` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin`	—	`sup_comm` `inf_comm` `boundary_le_boundary_sup_sup_boundary_inf_left`
`boundary_le_hnot` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `HNot.hnot` `CoheytingAlgebra.toHNot`	—	`inf_le_right`
`boundary_sup_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`boundary.eq_1` `inf_sup_right` `sup_le_sup` `inf_le_inf_left` `hnot_anti` `le_sup_left` `le_sup_right`
`boundary_sup_sup_boundary_inf` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `boundary` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`le_antisymm` `sup_le` `boundary_sup_le` `boundary_inf_le` `boundary_le_boundary_sup_sup_boundary_inf_left` `boundary_le_boundary_sup_sup_boundary_inf_right`
`boundary_top` 📖	mathematical	—	`boundary` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `CoheytingAlgebra.toOrderTop` `Bot.bot` `OrderBot.toBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `BoundedOrder.toOrderBot` `CoheytingAlgebra.toBoundedOrder`	—	`boundary.eq_1` `hnot_top` `inf_bot_eq`
`hnot_boundary` 📖	mathematical	—	`HNot.hnot` `CoheytingAlgebra.toHNot` `boundary` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `CoheytingAlgebra.toOrderTop`	—	`boundary.eq_1` `hnot_inf_distrib` `sup_hnot_self`
`hnot_eq_top_iff_exists_boundary` 📖	mathematical	—	`HNot.hnot` `CoheytingAlgebra.toHNot` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `CoheytingAlgebra.toOrderTop` `boundary`	—	`boundary.eq_1` `inf_top_eq` `hnot_boundary`
`hnot_hnot_sup_boundary` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `HNot.hnot` `CoheytingAlgebra.toHNot` `boundary`	—	`boundary.eq_1` `sup_inf_left` `hnot_sup_self` `inf_top_eq` `sup_eq_right` `hnot_hnot_le`
`inf_hnot_self` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `HNot.hnot` `CoheytingAlgebra.toHNot` `boundary`	—	—

Heyting

Definitions

Name	Category	Theorems
`«term∂_»` 📖	CompOp	—

---

← Back to Index