min_eq_of_lt — Mathlib

English

If a ∈ s and every b ∈ s with b ≠ a satisfies a < b, then hs.min (nonempty_of_mem a) = a.

Русский

Если a ∈ s и для всех b ∈ s, b ≠ a следует a < b, то минимальный элемент s равен a.

LaTeX

$$$hs.min\\, (nonempty_of_mem ha) = a$$$

Lean4

theorem min_eq_of_lt (hs : s.IsWF) (ha : a ∈ s) (hlt : ∀ b ∈ s, b ≠ a → a < b) : hs.min (nonempty_of_mem ha) = a :=
  by
  by_contra h
  exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha)) (hs.min_mem (nonempty_of_mem ha)) h)

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