iInf_eq_bot — Mathlib

English

Let f: ι → α with α a complete linear order. Then iInf f = ⊥ if and only if for every b > ⊥ there exists i with f(i) < b.

Русский

Пусть f: ι → α, α — полная линейная упорядоченная совокупность. Тогда iInf f = ⊥ тогда и только тогда, когда для каждого b > ⊥ существует i такой, что f(i) < b.

LaTeX

$$$\\displaystyle \\iinf f = \\bot \\iff \\forall b > \\bot, \\exists i, f(i) < b$$$

Lean4

theorem iInf_eq_bot (f : ι → α) : iInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b := by
  simp only [← sInf_range, sInf_eq_bot, Set.exists_range_iff]

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