Nucleus

📁 Source: Mathlib/Order/Nucleus.lean

Statistics

Metric	Count
Definitions `Nucleus`, `apply`, `giRestrict`, `instBot`, `instBoundedOrder`, `instCompleteLattice`, `instCompleteLatticeElemRangeCoe`, `instCompleteSemilatticeInf`, `instFrame`, `instFrameElemRangeCoe`, `instFunLike`, `instHImp`, `instHeytingAlgebra`, `instInfSet`, `instMin`, `instPartialOrder`, `instSemilatticeInf`, `instTop`, `instFrameMinimalAxioms`, `restrict`, `toClosureOperator`, `toInfHom`, `NucleusClass`	23
Theorems `bot_apply`, `coe_bot`, `coe_inf`, `coe_le_coe`, `coe_lt_coe`, `coe_mk`, `coe_toInfHom`, `coe_top`, `comp_eq_right_iff_le`, `ext`, `ext_iff`, `himp_apply`, `iInf_apply`, `idempotent`, `idempotent'`, `inf_apply`, `instNucleusClass`, `instTopHomClass`, `le_apply`, `le_apply'`, `map_himp_apply`, `map_himp_le`, `map_inf`, `mem_range`, `mk_le_mk`, `monotone`, `range_subset_range`, `restrict_toFun`, `sInf_apply`, `toFun_eq_coe`, `top_apply`, `idempotent`, `le_apply`, `toInfHomClass`	34
Total	57

Nucleus

Definitions

Name	Category	Theorems
`giRestrict` 📖	CompOp	—
`instBot` 📖	CompOp	2 math math: `coe_bot`, `bot_apply`
`instBoundedOrder` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instCompleteLatticeElemRangeCoe` 📖	CompOp	1 math math: `restrict_toFun`
`instCompleteSemilatticeInf` 📖	CompOp	—
`instFrame` 📖	CompOp	—
`instFrameElemRangeCoe` 📖	CompOp	—
`instFunLike` 📖	CompOp	32 math math: `instTopHomClass`, `instNucleusClass`, `coe_toInfHom`, `monotone`, `himp_apply`, `map_himp_apply`, `coe_inf`, `coe_mk`, `restrict_toFun`, `map_himp_le`, `mem_toSublocale`, `ext_iff`, `comp_eq_right_iff_le`, `coe_toSublocale`, `coe_lt_coe`, `range_subset_range`, `coe_bot`, `inf_apply`, `sInf_apply`, `mem_range`, `toFun_eq_coe`, `coe_le_coe`, `iInf_apply`, `idempotent`, `restrict_toSublocale`, `map_inf`, `coe_top`, `Sublocale.range_toNucleus`, `top_apply`, `Sublocale.toNucleus_apply`, `bot_apply`, `le_apply`
`instHImp` 📖	CompOp	1 math math: `himp_apply`
`instHeytingAlgebra` 📖	CompOp	—
`instInfSet` 📖	CompOp	2 math math: `sInf_apply`, `iInf_apply`
`instMin` 📖	CompOp	2 math math: `coe_inf`, `inf_apply`
`instPartialOrder` 📖	CompOp	11 math math: `comp_eq_right_iff_le`, `toSublocale_le_toSublocale`, `coe_lt_coe`, `range_subset_range`, `coe_bot`, `Sublocale.toNucleus_le_toNucleus`, `coe_le_coe`, `nucleusIsoSublocale.eq_toSublocale`, `nucleusIsoSublocale.symm_eq_toNucleus`, `mk_le_mk`, `bot_apply`
`instSemilatticeInf` 📖	CompOp	—
`instTop` 📖	CompOp	2 math math: `coe_top`, `top_apply`
`restrict` 📖	CompOp	1 math math: `restrict_toFun`
`toClosureOperator` 📖	CompOp	—
`toInfHom` 📖	CompOp	4 math math: `coe_toInfHom`, `idempotent'`, `toFun_eq_coe`, `le_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instBot`	—	—
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instBot`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `instMin` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin`	—	—
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe` `Nucleus` `instFunLike` `instPartialOrder`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe` `Nucleus` `instFunLike` `instPartialOrder`	—	—
`coe_mk` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfHom.toFun` `SemilatticeInf.toMin`	`DFunLike.coe` `Nucleus` `instFunLike` `InfHom` `InfHom.instFunLike`	—	—
`coe_toInfHom` 📖	mathematical	—	`DFunLike.coe` `InfHom` `SemilatticeInf.toMin` `InfHom.instFunLike` `toInfHom` `Nucleus` `instFunLike`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `Top.top` `instTop` `Pi.instTopForall` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`comp_eq_right_iff_le` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`coe_le_coe` `monotone` `le_apply` `le_antisymm` `le_trans` `idempotent'`
`ext` 📖	—	`DFunLike.coe` `Nucleus` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike`	—	`ext`
`himp_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike` `HImp.himp` `instHImp` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra`	—	—
`iInf_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `instFunLike` `iInf` `instInfSet` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iInf.eq_1` `sInf_apply` `iInf_range`
`idempotent` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike`	—	`ClosureOperator.idempotent`
`idempotent'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfHom.toFun` `SemilatticeInf.toMin` `toInfHom`	—	—
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `instMin` `SemilatticeInf.toMin`	—	—
`instNucleusClass` 📖	mathematical	—	`NucleusClass` `Nucleus` `instFunLike`	—	`InfHom.map_inf'` `idempotent'` `le_apply'`
`instTopHomClass` 📖	mathematical	—	`TopHomClass` `Nucleus` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLike`	—	`eq_top_iff` `le_apply`
`le_apply` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe` `Nucleus` `instFunLike`	—	`ClosureOperator.le_closure`
`le_apply'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfHom.toFun` `SemilatticeInf.toMin` `toInfHom`	—	—
`map_himp_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike` `HImp.himp` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra`	—	`le_antisymm` `LE.le.trans_eq` `map_himp_le` `idempotent` `le_apply`
`map_himp_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice` `DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `instFunLike` `HImp.himp` `GeneralizedHeytingAlgebra.toHImp` `HeytingAlgebra.toGeneralizedHeytingAlgebra` `Order.Frame.toHeytingAlgebra`	—	`le_himp_iff` `inf_le_inf` `le_refl` `le_apply` `map_inf` `himp_inf_self` `OrderHomClass.mono` `InfHomClass.toOrderHomClass` `NucleusClass.toInfHomClass` `instNucleusClass` `inf_le_left`
`map_inf` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `SemilatticeInf.toMin`	—	`InfHomClass.map_inf` `NucleusClass.toInfHomClass` `instNucleusClass`
`mem_range` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike`	—	`idempotent`
`mk_le_mk` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `InfHom.toFun` `SemilatticeInf.toMin`	`Nucleus` `instPartialOrder` `InfHom` `InfHom.instPartialOrder`	—	—
`monotone` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe` `Nucleus` `instFunLike`	—	`ClosureOperator.monotone`
`range_subset_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`mem_range` `Set.range_subset_iff` `monotone` `le_apply` `Set.range_subset_range_iff_exists_comp` `comp_eq_right_iff_le`
`restrict_toFun` 📖	mathematical	—	`DFunLike.coe` `FrameHom` `Set.Elem` `Set.range` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Order.Frame.toCompleteLattice` `instFunLike` `instCompleteLatticeElemRangeCoe` `FrameHom.instFunLike` `restrict` `Set.rangeFactorization`	—	—
`sInf_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `instFunLike` `InfSet.sInf` `instInfSet` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership`	—	—
`toFun_eq_coe` 📖	mathematical	—	`InfHom.toFun` `SemilatticeInf.toMin` `toInfHom` `DFunLike.coe` `Nucleus` `instFunLike`	—	—
`top_apply` 📖	mathematical	—	`DFunLike.coe` `Nucleus` `instFunLike` `Top.top` `instTop` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—

Nucleus.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

Nucleus.range

Definitions

Name	Category	Theorems
`instFrameMinimalAxioms` 📖	CompOp	—

NucleusClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`idempotent` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe`	—	—
`le_apply` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `DFunLike.coe`	—	—
`toInfHomClass` 📖	mathematical	—	`InfHomClass` `SemilatticeInf.toMin`	—	—

(root)

Definitions

Name	Category	Theorems
`Nucleus` 📖	CompData	37 math math: `Nucleus.instTopHomClass`, `Nucleus.instNucleusClass`, `Nucleus.coe_toInfHom`, `Nucleus.monotone`, `Nucleus.himp_apply`, `Nucleus.map_himp_apply`, `Nucleus.coe_inf`, `Nucleus.coe_mk`, `Nucleus.restrict_toFun`, `Nucleus.map_himp_le`, `Nucleus.mem_toSublocale`, `Nucleus.ext_iff`, `Nucleus.comp_eq_right_iff_le`, `Nucleus.coe_toSublocale`, `Nucleus.toSublocale_le_toSublocale`, `Nucleus.coe_lt_coe`, `Nucleus.range_subset_range`, `Nucleus.coe_bot`, `Nucleus.inf_apply`, `Nucleus.sInf_apply`, `Nucleus.mem_range`, `Nucleus.toFun_eq_coe`, `Sublocale.toNucleus_le_toNucleus`, `Nucleus.coe_le_coe`, `Nucleus.iInf_apply`, `nucleusIsoSublocale.eq_toSublocale`, `Nucleus.idempotent`, `nucleusIsoSublocale.symm_eq_toNucleus`, `Nucleus.restrict_toSublocale`, `Nucleus.map_inf`, `Nucleus.coe_top`, `Nucleus.mk_le_mk`, `Sublocale.range_toNucleus`, `Nucleus.top_apply`, `Sublocale.toNucleus_apply`, `Nucleus.bot_apply`, `Nucleus.le_apply`
`NucleusClass` 📖	CompData	1 math math: `Nucleus.instNucleusClass`

---

← Back to Index