Documentation Verification Report

WellFounded

📁 Source: Mathlib/Order/WellFounded.lean

Statistics

Metric	Count
Definitions `argmin`, `argminOn`, `min`, `sup`, `toOrderTop`, `toOrderBot`	6
Theorems `induction_bot`, `induction_bot'`, `argminOn_le`, `argminOn_mem`, `argmin_le`, `isMinimalFor_argmin`, `isMinimalFor_argminOn`, `not_lt_argmin`, `not_lt_argminOn`, `range_injOn_strictAnti`, `range_injOn_strictMono`, `range_inj`, `apply_le`, `id_le`, `le_apply`, `le_id`, `not_bddAbove_range_of_wellFoundedLT`, `not_bddBelow_range_of_wellFoundedGT`, `range_inj`, `instWellFoundedGT`, `instWellFoundedLT`, `asymm`, `has_min`, `induction_bot`, `induction_bot'`, `instAsymmRel_mathlib`, `irrefl`, `isAsymm`, `isIrrefl`, `lt_sup`, `min_le`, `min_mem`, `mono`, `not_lt_min`, `not_rel_apply_succ`, `onFun`, `wellFounded_iff_has_min`, `acc_def`, `acc_iff_isEmpty_descending_chain`, `exists_not_acc_lt_of_not_acc`, `not_acc_iff_exists_descending_chain`, `wellFounded_iff_isEmpty_descending_chain`	42
Total	48

Acc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction_bot` 📖	—	—	—	—	`induction_bot'`
`induction_bot'` 📖	—	—	—	—	`eq_or_ne`

Function

Definitions

Name	Category	Theorems
`argmin` 📖	CompOp	3 math math: `isMinimalFor_argmin`, `argmin_le`, `not_lt_argmin`
`argminOn` 📖	CompOp	5 math math: `sInf_eq_argmin_on`, `argminOn_mem`, `isMinimalFor_argminOn`, `argminOn_le`, `not_lt_argminOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`argminOn_le` 📖	mathematical	`Set` `Set.instMembership` `Set.Nonempty` `Set.nonempty_of_mem`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `argminOn` `Preorder.toLT`	—	`not_lt` `not_lt_argminOn`
`argminOn_mem` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `argminOn`	—	`WellFounded.min_mem`
`argmin_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `argmin` `Preorder.toLT`	—	`not_lt` `not_lt_argmin`
`isMinimalFor_argmin` 📖	mathematical	—	`MinimalFor` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.univ` `argmin` `Preorder.toLT`	—	`Set.mem_univ` `argmin_le`
`isMinimalFor_argminOn` 📖	mathematical	`Set.Nonempty`	`MinimalFor` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `argminOn` `Preorder.toLT`	—	`argminOn_mem` `argminOn_le`
`not_lt_argmin` 📖	mathematical	—	`argmin`	—	`WellFounded.not_lt_min` `wellFounded_lt` `Set.univ_nonempty` `Set.mem_univ`
`not_lt_argminOn` 📖	mathematical	`Set` `Set.instMembership` `Set.Nonempty` `Set.nonempty_of_mem`	`argminOn`	—	`WellFounded.not_lt_min` `wellFounded_lt`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_injOn_strictAnti` 📖	mathematical	—	`InjOn` `Set` `range` `setOf` `StrictAnti` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`range_injOn_strictMono` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `StrictAnti.dual`
`range_injOn_strictMono` 📖	mathematical	—	`InjOn` `Set` `range` `setOf` `StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`WellFoundedLT.induction` `mem_range_self` `lt_trichotomy` `Eq.not_lt` `StrictMono.injective` `StrictMono.lt_iff_lt`

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_inj` 📖	mathematical	`StrictAnti` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.range`	—	`Set.InjOn.eq_iff` `Set.range_injOn_strictAnti`

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`le_apply` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `dual`
`id_le` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pi.hasLe` `Preorder.toLE`	—	`Pi.le_def` `WellFounded.has_min` `wellFounded_lt` `Mathlib.Tactic.Push.not_forall_eq`
`le_apply` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE`	—	`id_le`
`le_id` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pi.hasLe` `Preorder.toLE`	—	`id_le` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `dual`
`not_bddAbove_range_of_wellFoundedLT` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`BddAbove` `Preorder.toLE` `Set.range`	—	`NoMaxOrder.exists_gt` `LT.lt.false` `LT.lt.trans_le` `LE.le.trans_lt` `le_apply` `Set.mem_range_self`
`not_bddBelow_range_of_wellFoundedGT` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`BddBelow` `Preorder.toLE` `Set.range`	—	`not_bddAbove_range_of_wellFoundedLT` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `OrderDual.noMaxOrder` `dual`
`range_inj` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.range`	—	`Set.InjOn.eq_iff` `Set.range_injOn_strictMono`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instWellFoundedGT` 📖	mathematical	—	`WellFoundedGT` `instLT_mathlib`	—	`instWellFoundedLT` `instWellFoundedLTOrderDualOfWellFoundedGT`
`instWellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `instLT_mathlib`	—	`IsWellFounded.wf`

WellFounded

Definitions

Name	Category	Theorems
`min` 📖	CompOp	4 math math: `min_mem`, `MvPowerSeries.lexOrder_def_of_ne_zero`, `min_le`, `not_lt_min`
`sup` 📖	CompOp	1 math math: `lt_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymm` 📖	—	—	—	—	`asymmetric`
`has_min` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership`	—	`not_imp_not`
`induction_bot` 📖	—	—	—	—	`induction_bot'`
`induction_bot'` 📖	—	—	—	—	`Acc.induction_bot'`
`instAsymmRel_mathlib` 📖	—	—	—	—	`asymm`
`irrefl` 📖	—	—	—	—	`Std.Asymm.irrefl` `asymm`
`isAsymm` 📖	—	—	—	—	`asymm`
`isIrrefl` 📖	—	—	—	—	`irrefl`
`lt_sup` 📖	mathematical	`Set.Bounded` `Set` `Set.instMembership`	`sup`	—	`min_mem`
`min_le` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instMembership` `Set.Nonempty`	`Preorder.toLE` `min`	—	`not_lt` `not_lt_min`
`min_mem` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `min`	—	`has_min`
`mono` 📖	—	—	—	—	—
`not_lt_min` 📖	mathematical	`Set.Nonempty` `Set` `Set.instMembership`	`min`	—	`has_min`
`not_rel_apply_succ` 📖	—	—	—	—	`wellFounded_iff_isEmpty_descending_chain` `IsWellFounded.wf`
`onFun` 📖	mathematical	—	`Function.onFun`	—	—
`wellFounded_iff_has_min` 📖	mathematical	—	`Set` `Set.instMembership`	—	`has_min`

WellFoundedGT

Definitions

Name	Category	Theorems
`toOrderTop` 📖	CompOp	—

WellFoundedLT

Definitions

Name	Category	Theorems
`toOrderBot` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc_def` 📖	—	—	—	—	—
`acc_iff_isEmpty_descending_chain` 📖	mathematical	—	`IsEmpty`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `nonempty_subtype` `not_acc_iff_exists_descending_chain`
`exists_not_acc_lt_of_not_acc` 📖	—	—	—	—	`Mathlib.Tactic.Push.not_forall_eq` `acc_def`
`not_acc_iff_exists_descending_chain` 📖	—	—	—	—	`exists_not_acc_lt_of_not_acc`
`wellFounded_iff_isEmpty_descending_chain` 📖	mathematical	—	`IsEmpty`	—	`IsEmpty.false` `acc_iff_isEmpty_descending_chain`

---

← Back to Index