Irreducible

📁 Source: Mathlib/Order/Irreducible.lean

Statistics

Metric	Count
Definitions `InfIrred`, `InfPrime`, `SupIrred`, `SupPrime`	4
Theorems `dual`, `finset_inf_eq`, `infPrime`, `ne_top`, `ofDual`, `dual`, `finset_inf_le`, `infIrred`, `inf_le`, `ne_top`, `ofDual`, `not_infIrred`, `not_infPrime`, `not_supIrred`, `not_supPrime`, `dual`, `finset_sup_eq`, `ne_bot`, `not_isMin`, `ofDual`, `supPrime`, `dual`, `le_finset_sup`, `le_sup`, `ne_bot`, `not_isMin`, `ofDual`, `supIrred`, `exists_infIrred_decomposition`, `exists_supIrred_decomposition`, `infIrred_iff_not_isMax`, `infIrred_ofDual`, `infIrred_toDual`, `infPrime_iff_infIrred`, `infPrime_iff_not_isMax`, `infPrime_ofDual`, `infPrime_toDual`, `not_infIrred`, `not_infIrred_top`, `not_infPrime`, `not_infPrime_top`, `not_supIrred`, `not_supIrred_bot`, `not_supPrime`, `not_supPrime_bot`, `supIrred_iff_not_isMin`, `supIrred_ofDual`, `supIrred_toDual`, `supPrime_iff_not_isMin`, `supPrime_iff_supIrred`, `supPrime_ofDual`, `supPrime_toDual`	52
Total	56

InfIrred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`InfIrred`	`SupIrred` `OrderDual` `OrderDual.instSemilatticeSup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`supIrred_toDual`
`finset_inf_eq` 📖	mathematical	`InfIrred` `Finset.inf`	`Finset` `Finset.instMembership`	—	`SupIrred.finset_sup_eq`
`infPrime` 📖	mathematical	`InfIrred` `Lattice.toSemilatticeInf` `DistribLattice.toLattice`	`InfPrime`	—	`infPrime_iff_infIrred`
`ne_top` 📖	—	`InfIrred`	—	—	`not_infIrred_top`
`ofDual` 📖	mathematical	`InfIrred` `OrderDual` `OrderDual.instSemilatticeInf`	`SupIrred` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`supIrred_ofDual`

InfPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`InfPrime`	`SupPrime` `OrderDual` `OrderDual.instSemilatticeSup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`supPrime_toDual`
`finset_inf_le` 📖	mathematical	`InfPrime`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Finset.inf` `Finset` `Finset.instMembership`	—	`SupPrime.le_finset_sup`
`infIrred` 📖	mathematical	`InfPrime`	`InfIrred`	—	`Eq.le`
`inf_le` 📖	mathematical	`InfPrime`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`inf_le_of_left_le` `inf_le_of_right_le`
`ne_top` 📖	—	`InfPrime`	—	—	`not_infPrime_top`
`ofDual` 📖	mathematical	`InfPrime` `OrderDual` `OrderDual.instSemilatticeInf`	`SupPrime` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`supPrime_ofDual`

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_infIrred` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`InfIrred`	—	—
`not_infPrime` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`InfPrime`	—	—

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_supIrred` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`SupIrred`	—	—
`not_supPrime` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`SupPrime`	—	—

SupIrred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`SupIrred`	`InfIrred` `OrderDual` `OrderDual.instSemilatticeInf` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`infIrred_toDual`
`finset_sup_eq` 📖	mathematical	`SupIrred` `Finset.sup`	`Finset` `Finset.instMembership`	—	`Finset.induction` `Finset.sup_empty` `ne_bot` `Finset.sup_insert`
`ne_bot` 📖	—	`SupIrred`	—	—	`not_supIrred_bot`
`not_isMin` 📖	mathematical	`SupIrred`	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	—
`ofDual` 📖	mathematical	`SupIrred` `OrderDual` `OrderDual.instSemilatticeSup`	`InfIrred` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`infIrred_ofDual`
`supPrime` 📖	mathematical	`SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice`	`SupPrime`	—	`supPrime_iff_supIrred`

SupPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	`SupPrime`	`InfPrime` `OrderDual` `OrderDual.instSemilatticeInf` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`infPrime_toDual`
`le_finset_sup` 📖	mathematical	`SupPrime`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Finset.sup` `Finset` `Finset.instMembership`	—	`Finset.induction` `Finset.sup_empty` `ne_bot` `Finset.sup_insert` `le_sup`
`le_sup` 📖	mathematical	`SupPrime`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`le_sup_of_le_left` `le_sup_of_le_right`
`ne_bot` 📖	—	`SupPrime`	—	—	`not_supPrime_bot`
`not_isMin` 📖	mathematical	`SupPrime`	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	—
`ofDual` 📖	mathematical	`SupPrime` `OrderDual` `OrderDual.instSemilatticeSup`	`InfPrime` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`infPrime_ofDual`
`supIrred` 📖	mathematical	`SupPrime`	`SupIrred`	—	`Eq.ge`

(root)

Definitions

Name	Category	Theorems
`InfIrred` 📖	MathDef	19 math math: `InfPrime.infIrred`, `OrderEmbedding.infIrredUpperSet_surjective`, `SupIrred.ofDual`, `supIrred_ofDual`, `IsMax.not_infIrred`, `OrderIso.infIrredUpperSet_symm_apply`, `not_infIrred`, `OrderEmbedding.infIrredUpperSet_apply`, `supIrred_toDual`, `UpperSet.infIrred_Ici`, `infIrred_iff_not_isMax`, `OrderIso.infIrredUpperSet_apply`, `exists_infIrred_decomposition`, `infIrred_toDual`, `infIrred_ofDual`, `UpperSet.infIrred_iff_of_finite`, `SupIrred.dual`, `infPrime_iff_infIrred`, `not_infIrred_top`
`InfPrime` 📖	MathDef	12 math math: `infPrime_iff_not_isMax`, `supPrime_toDual`, `infPrime_ofDual`, `not_infPrime_top`, `not_infPrime`, `SupPrime.dual`, `infPrime_toDual`, `InfIrred.infPrime`, `supPrime_ofDual`, `IsMax.not_infPrime`, `infPrime_iff_infIrred`, `SupPrime.ofDual`
`SupIrred` 📖	MathDef	26 math math: `OrderEmbedding.supIrredLowerSet_apply`, `OrderEmbedding.birkhoffFinset_inf`, `supIrred_ofDual`, `OrderEmbedding.coe_birkhoffFinset`, `OrderIso.supIrredLowerSet_symm_apply`, `exists_supIrred_decomposition`, `OrderEmbedding.birkhoffSet_inf`, `LowerSet.supIrred_iff_of_finite`, `supIrred_toDual`, `not_supIrred_bot`, `supIrred_iff_not_isMin`, `OrderIso.supIrredLowerSet_apply`, `InfIrred.dual`, `OrderEmbedding.supIrredLowerSet_surjective`, `SupPrime.supIrred`, `OrderEmbedding.birkhoffSet_sup`, `supPrime_iff_supIrred`, `infIrred_toDual`, `IsMin.not_supIrred`, `infIrred_ofDual`, `not_supIrred`, `LatticeHom.birkhoffFinset_injective`, `OrderEmbedding.birkhoffSet_apply`, `LowerSet.supIrred_Iic`, `OrderEmbedding.birkhoffFinset_sup`, `InfIrred.ofDual`
`SupPrime` 📖	MathDef	12 math math: `not_supPrime`, `SupIrred.supPrime`, `supPrime_toDual`, `infPrime_ofDual`, `InfPrime.dual`, `supPrime_iff_not_isMin`, `InfPrime.ofDual`, `infPrime_toDual`, `supPrime_iff_supIrred`, `IsMin.not_supPrime`, `supPrime_ofDual`, `not_supPrime_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_infIrred_decomposition` 📖	mathematical	—	`Finset.inf` `InfIrred`	—	`exists_supIrred_decomposition` `instWellFoundedLTOrderDualOfWellFoundedGT`
`exists_supIrred_decomposition` 📖	mathematical	—	`Finset.sup` `SupIrred`	—	`WellFoundedLT.induction` `Finset.sup_singleton` `not_supIrred` `Finset.sup_empty` `IsMin.eq_bot` `instIsEmptyFalse` `Finset.sup_union` `Finset.forall_mem_union`
`infIrred_iff_not_isMax` 📖	mathematical	—	`InfIrred` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`infIrred_ofDual` 📖	mathematical	—	`InfIrred` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `SupIrred` `OrderDual.instSemilatticeSup`	—	—
`infIrred_toDual` 📖	mathematical	—	`InfIrred` `OrderDual` `OrderDual.instSemilatticeInf` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `SupIrred`	—	—
`infPrime_iff_infIrred` 📖	mathematical	—	`InfPrime` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `InfIrred`	—	`InfPrime.infIrred` `sup_inf_left`
`infPrime_iff_not_isMax` 📖	mathematical	—	`InfPrime` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`infPrime_ofDual` 📖	mathematical	—	`InfPrime` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `SupPrime` `OrderDual.instSemilatticeSup`	—	—
`infPrime_toDual` 📖	mathematical	—	`InfPrime` `OrderDual` `OrderDual.instSemilatticeInf` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `SupPrime`	—	—
`not_infIrred` 📖	mathematical	—	`InfIrred` `IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `Preorder.toLT`	—	`not_supIrred`
`not_infIrred_top` 📖	mathematical	—	`InfIrred` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`IsMax.not_infIrred` `isMax_top`
`not_infPrime` 📖	mathematical	—	`InfPrime` `IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`not_supPrime`
`not_infPrime_top` 📖	mathematical	—	`InfPrime` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`IsMax.not_infPrime` `isMax_top`
`not_supIrred` 📖	mathematical	—	`SupIrred` `IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `Preorder.toLT`	—	`SupIrred.eq_1` `not_and_or` `Mathlib.Tactic.Push.not_forall_eq`
`not_supIrred_bot` 📖	mathematical	—	`SupIrred` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`IsMin.not_supIrred` `isMin_bot`
`not_supPrime` 📖	mathematical	—	`SupPrime` `IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`SupPrime.eq_1` `not_and_or` `Mathlib.Tactic.Push.not_forall_eq`
`not_supPrime_bot` 📖	mathematical	—	`SupPrime` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`IsMin.not_supPrime` `isMin_bot`
`supIrred_iff_not_isMin` 📖	mathematical	—	`SupIrred` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`supIrred_ofDual` 📖	mathematical	—	`SupIrred` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `InfIrred` `OrderDual.instSemilatticeInf`	—	—
`supIrred_toDual` 📖	mathematical	—	`SupIrred` `OrderDual` `OrderDual.instSemilatticeSup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `InfIrred`	—	—
`supPrime_iff_not_isMin` 📖	mathematical	—	`SupPrime` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`supPrime_iff_supIrred` 📖	mathematical	—	`SupPrime` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `SupIrred`	—	`SupPrime.supIrred` `inf_sup_left`
`supPrime_ofDual` 📖	mathematical	—	`SupPrime` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `InfPrime` `OrderDual.instSemilatticeInf`	—	—
`supPrime_toDual` 📖	mathematical	—	`SupPrime` `OrderDual` `OrderDual.instSemilatticeSup` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `InfPrime`	—	—

---

← Back to Index