min_le_min_of_subset — Mathlib

English

If s ⊆ t and both s and t are well-founded in a linear order, then the minimum of t is less than or equal to the minimum of s.

Русский

Если s ⊆ t и оба множества хорошо основаны в линейном порядке, то минимум t не больше минимума s.

LaTeX

$$$ht.min htn \le hs.min hsn$$$

Lean4

theorem min_le_min_of_subset {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s ⊆ t) :
    ht.min htn ≤ hs.min hsn :=
  (IsWF.le_min_iff _ _).2 fun _b hb => ht.min_le htn (hst hb)

Похожие утверждения