Documentation Verification Report

MonovaryOrder

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

Statistics

Metric	Count
Definitions `MonovaryOrder`	1
Theorems `exists_antitone_monotone`, `exists_monotone_antitone`, `exists_antitoneOn_monotoneOn`, `exists_monotoneOn_antitoneOn`, `exists_antitone`, `exists_monotone`, `exists_antitoneOn`, `exists_monotoneOn`, `antivaryOn_iff_exists_antitoneOn_monotoneOn`, `antivaryOn_iff_exists_monotoneOn_antitoneOn`, `antivary_iff_exists_antitone_monotone`, `antivary_iff_exists_monotone_antitone`, `instIsStrictTotalOrderMonovaryOrder`, `monovaryOn_iff_exists_antitoneOn`, `monovaryOn_iff_exists_monotoneOn`, `monovary_iff_exists_antitone`, `monovary_iff_exists_monotone`	17
Total	18

Antivary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antitone_monotone` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Antitone` `Monotone`	—	`antivary_iff_exists_antitone_monotone`
`exists_monotone_antitone` 📖	mathematical	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Monotone` `Antitone`	—	`antivary_iff_exists_monotone_antitone`

AntivaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antitoneOn_monotoneOn` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AntitoneOn` `MonotoneOn`	—	`antivaryOn_iff_exists_antitoneOn_monotoneOn`
`exists_monotoneOn_antitoneOn` 📖	mathematical	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MonotoneOn` `AntitoneOn`	—	`antivaryOn_iff_exists_monotoneOn_antitoneOn`

Monovary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antitone` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Antitone`	—	`monovary_iff_exists_antitone`
`exists_monotone` 📖	mathematical	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Monotone`	—	`monovary_iff_exists_monotone`

MonovaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antitoneOn` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AntitoneOn`	—	`monovaryOn_iff_exists_antitoneOn`
`exists_monotoneOn` 📖	mathematical	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MonotoneOn`	—	`monovaryOn_iff_exists_monotoneOn`

(root)

Definitions

Name	Category	Theorems
`MonovaryOrder` 📖	MathDef	1 math math: `instIsStrictTotalOrderMonovaryOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antivaryOn_iff_exists_antitoneOn_monotoneOn` 📖	mathematical	—	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AntitoneOn` `MonotoneOn`	—	—
`antivaryOn_iff_exists_monotoneOn_antitoneOn` 📖	mathematical	—	`AntivaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MonotoneOn` `AntitoneOn`	—	—
`antivary_iff_exists_antitone_monotone` 📖	mathematical	—	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Antitone` `Monotone`	—	—
`antivary_iff_exists_monotone_antitone` 📖	mathematical	—	`Antivary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monotone` `Antitone`	—	—
`instIsStrictTotalOrderMonovaryOrder` 📖	mathematical	—	`IsStrictTotalOrder` `MonovaryOrder`	—	`trichotomous_of` `Prod.trichotomous` `instTrichotomousLt` `IsWellOrder.toTrichotomous` `WellOrderingRel.isWellOrder` `MonovaryOrder.eq_1` `irrefl` `Prod.instIrreflLex_mathlib` `instIrreflLt` `IsStrictOrder.toIrrefl` `IsStrictTotalOrder.toIsStrictOrder` `instIsStrictTotalOrderOfIsWellOrder` `trans` `Prod.instIsTransLex` `instIsTransLt` `IsWellOrder.toIsTrans`
`monovaryOn_iff_exists_antitoneOn` 📖	mathematical	—	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AntitoneOn`	—	—
`monovaryOn_iff_exists_monotoneOn` 📖	mathematical	—	`MonovaryOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MonotoneOn`	—	`instIsStrictTotalOrderMonovaryOrder` `monotoneOn_iff_forall_lt` `Prod.lex_iff` `LT.lt.le` `Eq.le` `MonovaryOn.symm` `MonotoneOn.monovaryOn`
`monovary_iff_exists_antitone` 📖	mathematical	—	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Antitone`	—	—
`monovary_iff_exists_monotone` 📖	mathematical	—	`Monovary` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monotone`	—	—

---

← Back to Index