Union

📁 Source: Mathlib/Order/Monotone/Union.lean

Statistics

Metric	Count
Definitions	0
Theorems Iic_union_Ici, union_right, Iic_union_Ici, union_right, Iic_union_Ici, union, Iic_union_Ici, union	8
Total	8

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_union_Ici 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic Set.Ici	Antitone	—	Monotone.dual_right MonotoneOn.Iic_union_Ici dual_right
union_right 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGreatest Preorder.toLE IsLeast	Set Set.instUnion	—	MonotoneOn.dual_right MonotoneOn.union_right dual_right

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_union_Ici 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic Set.Ici	Monotone	—	monotoneOn_univ Set.Iic_union_Ici union_right isGreatest_Iic isLeast_Ici
union_right 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGreatest Preorder.toLE IsLeast	Set Set.instUnion	—	eq_or_lt_of_le lt_irrefl LT.lt.trans_le lt_or_ge LT.lt.le LE.le.trans

StrictAntiOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_union_Ici 📖	mathematical	StrictAntiOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic Set.Ici	StrictAnti	—	StrictMono.dual_right StrictMonoOn.Iic_union_Ici dual_right
union 📖	mathematical	StrictAntiOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGreatest Preorder.toLE IsLeast	Set Set.instUnion	—	StrictMonoOn.dual_right StrictMonoOn.union dual_right

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_union_Ici 📖	mathematical	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Iic Set.Ici	StrictMono	—	strictMonoOn_univ Set.Iic_union_Ici union isGreatest_Iic isLeast_Ici
union 📖	mathematical	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsGreatest Preorder.toLE IsLeast	Set Set.instUnion	—	eq_or_lt_of_le lt_irrefl LT.lt.trans_le lt_or_ge LT.lt.le monotoneOn LE.le.trans

---

← Back to Index