English
For a finite set s and a function f: ι → α, if there exists x ∈ s with sSup ∅ ≤ f(x), then the supremum of the values f(i) over i ∈ s is less than a if and only if every f(x) with x ∈ s is less than a.
Русский
Для конечного множества s и функции f: ι → α существует x ∈ s с sSup ∅ ≤ f(x); тогда наименьшее верхнее значение по i∈s удовлетворяет равенству: ⨆ i∈s f(i) < a тогда и только если для каждого x ∈ s выполняется f(x) < a.
LaTeX
$$$⨆ i∈s, f(i) < a \iff ∀ x∈s, f(x) < a.$$$
Lean4
theorem ciSup_lt_iff {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) :
⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a := by
constructor
· intro h x hx
refine h.trans_le' (le_csSup ?_ ?_)
·
classical
refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
intro
simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image, forall_exists_index]
grind
· simp only [mem_range]
refine ⟨x, ?_⟩
simp [hx]
· have := hs.ciSup_mem_image _ h
grind
