min_of_subset_not_lt_min — Mathlib

English

If s ⊆ t and both s and t are WF with nonempty, then the minimal elements are ordered so that hs.min hsn is not below ht.min htn.

Русский

Если s ⊆ t и оба множества хорошо основаны, то минимальные элементы имеют соответствие: hs.min hsn не меньше ht.min htn.

LaTeX

$$$hs \\subseteq ht \\Rightarrow \\neg\\bigl( hs.min\\, hsn < ht.min\\, htn \\bigr)$$$

Lean4

theorem min_of_subset_not_lt_min {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s ⊆ t) :
    ¬hs.min hsn < ht.min htn :=
  ht.not_lt_min htn (hst (min_mem hs hsn))

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