lt_sup'_iff — Mathlib

English

Let s be 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 < s.sup' H f \iff \exists b \in s, a < f(b).$$$

Lean4

@[simp]
theorem lt_sup'_iff : a < s.sup' H f ↔ ∃ b ∈ s, a < f b :=
  by
  rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
  exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

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