Order

📁 Source: Mathlib/Data/Set/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems inter, union, inter, union, inter, union, inter, union, antitoneOn_iff_antitone, antitone_bforall, antitone_setOf, monotoneOn_iff_monotone, monotone_setOf, not_monotoneOn_not_antitoneOn_iff_exists_le_le, not_monotoneOn_not_antitoneOn_iff_exists_lt_lt, strictAntiOn_iff_strictAnti, strictMonoOn_iff_strictMono	17
Total	17

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	Antitone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instInter	—	inf
union 📖	mathematical	Antitone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instUnion	—	sup

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	AntitoneOn Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instInter	—	inf
union 📖	mathematical	AntitoneOn Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instUnion	—	sup

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	Monotone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instInter	—	inf
union 📖	mathematical	Monotone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instUnion	—	sup

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	MonotoneOn Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instInter	—	inf
union 📖	mathematical	MonotoneOn Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice Set.instDistribLattice	Set.instUnion	—	sup

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_iff_antitone 📖	mathematical	—	AntitoneOn Antitone Elem Subtype.preorder Set instMembership	—	—
antitone_bforall 📖	mathematical	—	Antitone Set PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLattice Prop.partialOrder	—	—
antitone_setOf 📖	mathematical	Antitone PartialOrder.toPreorder Prop.partialOrder	Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLattice setOf	—	—
monotoneOn_iff_monotone 📖	mathematical	—	MonotoneOn Monotone Elem Subtype.preorder Set instMembership	—	—
monotone_setOf 📖	mathematical	Monotone PartialOrder.toPreorder Prop.partialOrder	Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLattice setOf	—	—
not_monotoneOn_not_antitoneOn_iff_exists_le_le 📖	mathematical	—	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AntitoneOn Set instMembership Preorder.toLE Preorder.toLT	—	—
not_monotoneOn_not_antitoneOn_iff_exists_lt_lt 📖	mathematical	—	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AntitoneOn Set instMembership Preorder.toLT	—	—
strictAntiOn_iff_strictAnti 📖	mathematical	—	StrictAntiOn StrictAnti Elem Subtype.preorder Set instMembership	—	—
strictMonoOn_iff_strictMono 📖	mathematical	—	StrictMonoOn StrictMono Elem Subtype.preorder Set instMembership	—	—

---

← Back to Index