max_of_mem — Mathlib

English

If a ∈ s, then there exists b ∈ α such that s.max = b (i.e., the maximum is attained by some element of the set).

Русский

Если a ∈ s, то существует b ∈ α такое, что s.max = b (то есть максимум достигается элементом множества).

LaTeX

$$$$ a \\in s \\Rightarrow \\exists b \\in \\alpha, \\, s.max = b. $$$$

Lean4

theorem max_of_mem {s : Finset α} {a : α} (h : a ∈ s) : ∃ b : α, s.max = b :=
  by
  obtain ⟨b, h, _⟩ := le_sup (α := WithBot α) h _ rfl
  exact ⟨b, h⟩

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