Disjointed

📁 Source: Mathlib/Algebra/Order/Disjointed.lean

Statistics

Metric	Count
Definitions disjointedRec	1
Theorems disjointed_add_one, disjointed_add_one_sup, disjointedRec_zero, disjointed_add_one, partialSups_add_one_eq_sup_disjointed	5
Total	6

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjointed_add_one 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	disjointed GeneralizedBooleanAlgebra.toSDiff	—	Order.succ_eq_add_one disjointed_succ not_isMax
disjointed_add_one_sup 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	SemilatticeSup.toMax Lattice.toSemilatticeSup disjointed	—	Order.succ_eq_add_one disjointed_succ_sup

Nat

Definitions

Name	Category	Theorems
disjointedRec 📖	CompOp	1 math math: disjointedRec_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjointedRec_zero 📖	mathematical	—	Nat.disjointedRec disjointed Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder disjointed_zero	—	—
disjointed_add_one 📖	mathematical	—	disjointed PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder GeneralizedBooleanAlgebra.toSDiff DFunLike.coe OrderHom SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra OrderHom.instFunLike partialSups	—	Order.succ_eq_add_one disjointed_succ not_isMax
partialSups_add_one_eq_sup_disjointed 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra OrderHom.instFunLike partialSups SemilatticeSup.toMax disjointed	—	Order.succ_eq_add_one Order.le_succ le_antisymm le_trans le_partialSups le_sup_right disjointed_succ partialSups_succ sup_sdiff_self

---

← Back to Index