le_sup'_iff — Mathlib

English

Let s be a nonempty finite subset of α and f: ι → α. Then a ≤ s.sup' H f iff there exists b ∈ s with a ≤ f(b).

Русский

Пусть s непустое конечное подмножество и f: ι → α. Тогда a ≤ sup' f над s эквивалентно существованию b ∈ s с a ≤ f(b).

LaTeX

$$$a \le s.sup' H f \iff \exists b \in s, a \le f(b).$$$

Lean4

@[simp]
theorem le_sup'_iff : a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b :=
  by
  rw [← WithBot.coe_le_coe, coe_sup', Finset.le_sup_iff (WithBot.bot_lt_coe a)]
  exact exists_congr (fun _ => and_congr_right' WithBot.coe_le_coe)

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