min_eq_of_le — Mathlib

English

If a ∈ s and a ≤ b for all b ∈ s, then hs.min (nonempty_of_mem ha) = a.

Русский

Если a ∈ s и a ≤ b для всех b ∈ s, тогда hs.min (nonempty_of_mem ha) = a.

LaTeX

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

Lean4

theorem min_eq_of_le (hs : s.IsWF) (ha : a ∈ s) (hle : ∀ b ∈ s, a ≤ b) : hs.min (nonempty_of_mem ha) = a :=
  (eq_of_le_of_not_lt (hle (hs.min (nonempty_of_mem ha)) (hs.min_mem (nonempty_of_mem ha)))
      (hs.not_lt_min (nonempty_of_mem ha) ha)).symm

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