iInf_coe_lt_top — Mathlib

English

Let ι be a type and f : ι → ℕ. Then the infimum of the family (f i) in the extended natural numbers is strictly less than the top element if and only if ι is nonempty.

Русский

Пусть ι — произвольный тип индексов и f : ι → ℕ. Тогда наименьшая нижняя грань семейства (f i) в расширенном множестве натуральных чисел меньше вершины ⊤ тогда и только тогда, когда ι непусто.

LaTeX

$$$\inf_{i} (f(i) : \mathbb{N}_\infty) < \top \;\iff\; \iota \neq \varnothing$$$

Lean4

theorem iInf_coe_lt_top : ⨅ i, (f i : ℕ∞) < ⊤ ↔ Nonempty ι :=
  WithTop.iInf_coe_lt_top

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