Extension

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

Statistics

Metric	Count
Definitions	0
Theorems exists_antitone_extension, exists_monotone_extension	2
Total	2

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_antitone_extension 📖	mathematical	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice BddBelow Preorder.toLE Set.image BddAbove	Antitone Set.EqOn	—	MonotoneOn.exists_monotone_extension dual_right

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_monotone_extension 📖	mathematical	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice BddBelow Preorder.toLE Set.image BddAbove	Monotone Set.EqOn	—	BddAbove.mono Set.image_mono Set.inter_subset_right Set.self_mem_Iic Set.Nonempty.not_disjoint IsGreatest.nonempty IsGreatest.csSup_eq map_isGreatest mono instReflLe Set.not_disjoint_iff_nonempty_inter le_csSup_of_le Set.mem_image_of_mem Disjoint.mono_left Set.Iic_subset_Iic csSup_le_csSup Set.Nonempty.image Set.inter_subset_inter subset_refl Set.instReflSubset

---

← Back to Index