sup_of_mem — Mathlib

English

Let s be a finite nonempty set of β and f : β → α with α a SemilatticeSup. Then the supremum over s of f is equal to f(b) for some b ∈ s.

Русский

Пусть s — конечное непустое множество β и f : β → α; существует элемент b ∈ s, для которого sup' f равен f(b).

LaTeX

$$$\exists b \in s, \ s.sup' f = f(b)$$$

Lean4

theorem sup_of_mem {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ a : α, s.sup ((↑) ∘ f : β → WithBot α) = ↑a :=
  Exists.imp (fun _ => And.left) (@le_sup (WithBot α) _ _ _ _ _ _ h (f b) rfl)

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