Mathlib Map

Theorems · Theorem · order theory

WellFounded.min_le

∀ {β : Type u_2} [inst : LinearOrder β] (h : WellFounded fun x1 x2 => x1 < x2) {x : β} {s : Set β} (hx : x ∈ s),
  h.min s ⋯ ≤ x
Defined in
Mathlib.Order.WellFounded
Cited by
2 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Field.Emb.Cardinal.isLeast_leastExt · cited by 4Cardinal.isLeast_leastExtIsUpperSet.eq_empty_or_Ici · cited by 2IsUpperSet.eq_empty_or_IciSet · cited by 53352SetLinearOrder · cited by 8572LinearOrdernot_lt · cited by 306not_ltWellFounded.min · cited by 33WellFounded.minWellFounded.not_lt_min · cited by 20WellFounded.not_lt_minWellFounded.min_leCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.