Monotone

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

Statistics

Metric	Count
Definitions	0
Theorems mono, monotone, antitoneOn_of_rightInvOn_of_mapsTo, monotoneOn_of_rightInvOn_of_mapsTo, codRestrict, rangeFactorization, restrict, mono, monotone, congr_antitoneOn, congr_monotoneOn, congr_strictAntiOn, congr_strictMonoOn, antitoneOn_insert_iff, monotoneOn_insert_iff, mono, strictAnti, codRestrict, of_restrict, mono, restrict, strictMono, strictAntiOn_insert_iff, strictAntiOn_insert_iff_of_forall_ge, strictAntiOn_insert_iff_of_forall_le, strictMonoOn_insert_iff, strictMonoOn_insert_iff_of_forall_ge, strictMonoOn_insert_iff_of_forall_le, strictMono_restrict	29
Total	29

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	AntitoneOn Set Set.instHasSubset	—	—	—
monotone 📖	mathematical	AntitoneOn	Antitone Set.Elem Subtype.preorder Set Set.instMembership	—	Subtype.coe_prop

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_of_rightInvOn_of_mapsTo 📖	—	AntitoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.RightInvOn Set.MapsTo	—	—	MonotoneOn.dual_right monotoneOn_of_rightInvOn_of_mapsTo AntitoneOn.dual_left
monotoneOn_of_rightInvOn_of_mapsTo 📖	—	MonotoneOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.RightInvOn Set.MapsTo	—	—	le_total le_refl le_antisymm Set.RightInvOn.eq

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	Monotone Set Set.instMembership	Set.Elem Subtype.preorder Set.codRestrict	—	—
rangeFactorization 📖	mathematical	Monotone	Set.Elem Set.range Subtype.preorder Set Set.instMembership Set.rangeFactorization	—	—
restrict 📖	mathematical	Monotone	Set.Elem Subtype.preorder Set Set.instMembership Set.restrict	—	—

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	MonotoneOn Set Set.instHasSubset	—	—	—
monotone 📖	mathematical	MonotoneOn	Monotone Set.Elem Subtype.preorder Set Set.instMembership	—	Subtype.coe_prop

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitoneOn_insert_iff 📖	mathematical	—	AntitoneOn Set instInsert Preorder.toLE	—	monotoneOn_insert_iff
monotoneOn_insert_iff 📖	mathematical	—	MonotoneOn Set instInsert Preorder.toLE	—	—

Set.EqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_antitoneOn 📖	mathematical	Set.EqOn	AntitoneOn	—	AntitoneOn.congr symm
congr_monotoneOn 📖	mathematical	Set.EqOn	MonotoneOn	—	MonotoneOn.congr symm
congr_strictAntiOn 📖	mathematical	Set.EqOn	StrictAntiOn	—	StrictAntiOn.congr symm
congr_strictMonoOn 📖	mathematical	Set.EqOn	StrictMonoOn	—	StrictMonoOn.congr symm

StrictAntiOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	StrictAntiOn Set Set.instHasSubset	—	—	—
strictAnti 📖	mathematical	StrictAntiOn	StrictAnti Set.Elem Subtype.preorder Set Set.instMembership	—	Subtype.coe_prop

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict 📖	mathematical	StrictMono Set Set.instMembership	Set.Elem Subtype.preorder Set.codRestrict	—	—
of_restrict 📖	mathematical	StrictMono Set.Elem Subtype.preorder Set Set.instMembership Set.restrict	StrictMonoOn	—	strictMono_restrict

StrictMonoOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	StrictMonoOn Set Set.instHasSubset	—	—	—
restrict 📖	mathematical	StrictMonoOn	StrictMono Set.Elem Subtype.preorder Set Set.instMembership Set.restrict	—	strictMono_restrict
strictMono 📖	mathematical	StrictMonoOn	StrictMono Set.Elem Subtype.preorder Set Set.instMembership	—	Subtype.coe_prop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictAntiOn_insert_iff 📖	mathematical	—	StrictAntiOn Set Set.instInsert Preorder.toLT	—	strictMonoOn_insert_iff
strictAntiOn_insert_iff_of_forall_ge 📖	mathematical	Preorder.toLE	StrictAntiOn Set Set.instInsert Preorder.toLT	—	strictAntiOn_insert_iff LE.le.not_gt
strictAntiOn_insert_iff_of_forall_le 📖	mathematical	Preorder.toLE	StrictAntiOn Set Set.instInsert Preorder.toLT	—	strictAntiOn_insert_iff LE.le.not_gt
strictMonoOn_insert_iff 📖	mathematical	—	StrictMonoOn Set Set.instInsert Preorder.toLT	—	—
strictMonoOn_insert_iff_of_forall_ge 📖	mathematical	Preorder.toLE	StrictMonoOn Set Set.instInsert Preorder.toLT	—	strictMonoOn_insert_iff LE.le.not_gt
strictMonoOn_insert_iff_of_forall_le 📖	mathematical	Preorder.toLE	StrictMonoOn Set Set.instInsert Preorder.toLT	—	strictMonoOn_insert_iff LE.le.not_gt
strictMono_restrict 📖	mathematical	—	StrictMono Set.Elem Subtype.preorder Set Set.instMembership Set.restrict StrictMonoOn	—	—

---

← Back to Index