lt_biSup_iff — Mathlib

English

For a set s and a function f on s, a is less than the bi-supremum over s exactly when there exists i ∈ s with a < f(i).

Русский

Для множества s и функции f на s: a меньше biSup s f тогда и только тогда, когда существует i ∈ s такое, что a < f(i).

LaTeX

$$$a < \big\vee\_{i \in s} f(i) \;\iff\; \exists i \in s, a < f(i)$$$

Lean4

theorem lt_biSup_iff {s : Set β} {f : β → α} : a < ⨆ i ∈ s, f i ↔ ∃ i ∈ s, a < f i := by simp [lt_iSup_iff]

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