not_lt_min — Mathlib

English

If s is well-founded and nonempty and a ∈ s, then a is not less than the minimal element of s.

Русский

Если s хорошо основано, непусто и a ∈ s, то a не меньше минимального элемента s.

LaTeX

$$$\\neg\\bigl(a < hs.min\\, hn\\bigr)$$$

Lean4

nonrec theorem not_lt_min (hs : IsWF s) (hn : s.Nonempty) (ha : a ∈ s) : ¬a < hs.min hn :=
  hs.not_lt_min univ (nonempty_iff_univ_nonempty.1 hn.to_subtype) (mem_univ (⟨a, ha⟩ : s))

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