Documentation Verification Report

Regular

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

Statistics

Metric	Count
Definitions `ofRegular`, `IsRegular`, `decidablePred`, `Regular`, `bot`, `boundedOrder`, `gi`, `himp`, `inf`, `instBooleanAlgebra`, `instCoeOut`, `instCompl`, `instInhabited`, `instPartialOrder`, `lattice`, `toRegular`, `top`, `val`	18
Theorems `disjoint_compl_left_iff`, `disjoint_compl_right_iff`, `eq`, `himp`, `inf`, `coe_bot`, `coe_compl`, `coe_himp`, `coe_inf`, `coe_inj`, `coe_injective`, `coe_le_coe`, `coe_lt_coe`, `coe_sdiff`, `coe_sup`, `coe_toRegular`, `coe_top`, `prop`, `toRegular_coe`, `isRegular_bot`, `isRegular_compl`, `isRegular_of_boolean`, `isRegular_of_decidable`, `isRegular_top`	24
Total	42

BooleanAlgebra

Definitions

Name	Category	Theorems
`ofRegular` 📖	CompOp	—

Heyting

Definitions

Name	Category	Theorems
`IsRegular` 📖	MathDef	6 math math: `isRegular_top`, `isRegular_of_boolean`, `Regular.prop`, `isRegular_compl`, `isRegular_bot`, `isRegular_of_decidable`
`Regular` 📖	CompOp	12 math math: `Regular.coe_himp`, `Regular.coe_sdiff`, `Regular.coe_le_coe`, `Regular.coe_inf`, `Regular.coe_bot`, `Regular.coe_injective`, `Regular.coe_top`, `Regular.coe_toRegular`, `Regular.coe_lt_coe`, `Regular.toRegular_coe`, `Regular.coe_sup`, `Regular.coe_compl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_bot` 📖	mathematical	—	`IsRegular` `HeytingAlgebra.toCompl` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `HeytingAlgebra.toOrderBot`	—	`IsRegular.eq_1` `compl_bot` `compl_top`
`isRegular_compl` 📖	mathematical	—	`IsRegular` `HeytingAlgebra.toCompl` `Compl.compl`	—	`compl_compl_compl`
`isRegular_of_boolean` 📖	mathematical	—	`IsRegular` `BooleanAlgebra.toCompl`	—	`compl_compl`
`isRegular_of_decidable` 📖	mathematical	—	`IsRegular` `Prop.instCompl`	—	—
`isRegular_top` 📖	mathematical	—	`IsRegular` `HeytingAlgebra.toCompl` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `BoundedOrder.toOrderTop` `HeytingAlgebra.toBoundedOrder`	—	`IsRegular.eq_1` `compl_top` `compl_bot`

Heyting.IsRegular

Definitions

Name	Category	Theorems
`decidablePred` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_compl_left_iff` 📖	mathematical	`Heyting.IsRegular` `HeytingAlgebra.toCompl`	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `HeytingAlgebra.toOrderBot` `Compl.compl` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_compl_iff_disjoint_left` `eq`
`disjoint_compl_right_iff` 📖	mathematical	`Heyting.IsRegular` `HeytingAlgebra.toCompl`	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `HeytingAlgebra.toOrderBot` `Compl.compl` `Preorder.toLE` `PartialOrder.toPreorder`	—	`le_compl_iff_disjoint_right` `eq`
`eq` 📖	mathematical	`Heyting.IsRegular`	`Compl.compl`	—	—
`himp` 📖	mathematical	`Heyting.IsRegular` `HeytingAlgebra.toCompl`	`HImp.himp` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra`	—	`eq_1` `compl_compl_himp_distrib` `eq`
`inf` 📖	mathematical	`Heyting.IsRegular` `HeytingAlgebra.toCompl`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra`	—	`eq_1` `compl_compl_inf_distrib` `eq`

Heyting.Regular

Definitions

Name	Category	Theorems
`bot` 📖	CompOp	1 math math: `coe_bot`
`boundedOrder` 📖	CompOp	—
`gi` 📖	CompOp	—
`himp` 📖	CompOp	1 math math: `coe_himp`
`inf` 📖	CompOp	1 math math: `coe_inf`
`instBooleanAlgebra` 📖	CompOp	1 math math: `coe_sdiff`
`instCoeOut` 📖	CompOp	—
`instCompl` 📖	CompOp	1 math math: `coe_compl`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	4 math math: `coe_le_coe`, `coe_toRegular`, `coe_lt_coe`, `toRegular_coe`
`lattice` 📖	CompOp	1 math math: `coe_sup`
`toRegular` 📖	CompOp	2 math math: `coe_toRegular`, `toRegular_coe`
`top` 📖	CompOp	1 math math: `coe_top`
`val` 📖	CompOp	14 math math: `coe_himp`, `coe_sdiff`, `coe_inj`, `coe_le_coe`, `coe_inf`, `coe_bot`, `coe_injective`, `coe_top`, `prop`, `coe_toRegular`, `coe_lt_coe`, `toRegular_coe`, `coe_sup`, `coe_compl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`val` `Bot.bot` `Heyting.Regular` `bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `HeytingAlgebra.toOrderBot`	—	—
`coe_compl` 📖	mathematical	—	`val` `Compl.compl` `Heyting.Regular` `instCompl` `HeytingAlgebra.toCompl`	—	—
`coe_himp` 📖	mathematical	—	`val` `HImp.himp` `Heyting.Regular` `himp` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra`	—	—
`coe_inf` 📖	mathematical	—	`val` `Heyting.Regular` `inf` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra`	—	—
`coe_inj` 📖	mathematical	—	`val`	—	—
`coe_injective` 📖	mathematical	—	`Heyting.Regular` `val`	—	`Subtype.coe_injective`
`coe_le_coe` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `val` `Heyting.Regular` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `val` `Heyting.Regular` `instPartialOrder`	—	—
`coe_sdiff` 📖	mathematical	—	`val` `Heyting.Regular` `BooleanAlgebra.toSDiff` `instBooleanAlgebra` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Compl.compl` `HeytingAlgebra.toCompl`	—	—
`coe_sup` 📖	mathematical	—	`val` `Heyting.Regular` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `lattice` `Compl.compl` `HeytingAlgebra.toCompl` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra`	—	—
`coe_toRegular` 📖	mathematical	—	`val` `DFunLike.coe` `OrderHom` `Heyting.Regular` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `instPartialOrder` `OrderHom.instFunLike` `toRegular` `Compl.compl` `HeytingAlgebra.toCompl`	—	—
`coe_top` 📖	mathematical	—	`val` `Top.top` `Heyting.Regular` `top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `BoundedOrder.toOrderTop` `HeytingAlgebra.toBoundedOrder`	—	—
`prop` 📖	mathematical	—	`Heyting.IsRegular` `HeytingAlgebra.toCompl` `val`	—	`Subtype.prop`
`toRegular_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Heyting.Regular` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedHeytingAlgebra.toLattice` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `instPartialOrder` `OrderHom.instFunLike` `toRegular` `val`	—	`coe_injective`

---

← Back to Index