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, asymm, has_min, induction_bot, induction_bot', instAsymmRel_mathlib, irrefl, isAsymm, isIrrefl, lt_sup, mem_of_lt_min_compl, min_eq_of_forall_not_lt, min_le, min_mem, mono, notMem_of_lt_min, not_lt_min, not_rel_apply_succ, onFun, prop_min, wellFounded_iff_has_min, acc_def, acc_iff_isEmpty_descending_chain, exists_not_acc_lt_of_not_acc, instWellFoundedGTULift, instWellFoundedLTULift, not_acc_iff_exists_descending_chain, wellFounded_iff_isEmpty_descending_chain	46
Total	52

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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder argminOn Preorder.toLT Set Set.instMembership	—	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 argmin Preorder.toLT	—	argmin_le
isMinimalFor_argminOn 📖	mathematical	Set.Nonempty	MinimalFor Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership argminOn Preorder.toLT	—	argminOn_mem argminOn_le
not_lt_argmin 📖	mathematical	—	argmin	—	WellFounded.not_lt_min wellFounded_lt Set.mem_univ
not_lt_argminOn 📖	mathematical	Set Set.instMembership	argminOn Set Set.instMembership	—	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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	id_le
le_id 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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

WellFounded

Definitions

Name	Category	Theorems
min 📖	CompOp	10 math math: min_mem, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, Ordinal.card_typein_min_le_mk, MvPowerSeries.lexOrder_def_of_ne_zero, prop_min, cardinalMk_subtype_lt_min_compl_le, min_le, min_eq_of_forall_not_lt, Ordinal.not_lt_enum_ord_mk_min_compl, 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
mem_of_lt_min_compl 📖	mathematical	Set.Nonempty Compl.compl Set Set.instCompl min	Set Set.instMembership	—	Set.notMem_compl_iff notMem_of_lt_min
min_eq_of_forall_not_lt 📖	mathematical	Set Set.instMembership	min Set Set.instMembership	—	min_mem not_lt_min
min_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder min Preorder.toLT Set Set.instMembership	—	not_lt not_lt_min
min_mem 📖	mathematical	Set.Nonempty	Set Set.instMembership min	—	has_min
mono 📖	—	—	—	—	—
notMem_of_lt_min 📖	mathematical	Set.Nonempty min	Set Set.instMembership	—	not_lt_min
not_lt_min 📖	mathematical	Set Set.instMembership	min Set Set.instMembership	—	has_min
not_rel_apply_succ 📖	—	—	—	—	wellFounded_iff_isEmpty_descending_chain IsWellFounded.wf
onFun 📖	mathematical	—	Function.onFun	—	—
prop_min 📖	mathematical	—	min setOf	—	min_mem
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
instWellFoundedGTULift 📖	mathematical	—	WellFoundedGT ULift.instLT_mathlib	—	IsWellFounded.wf
instWellFoundedLTULift 📖	mathematical	—	WellFoundedLT ULift.instLT_mathlib	—	IsWellFounded.wf
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