iInf_le_iff — Mathlib

English

For a family indexed by ι taking values in α (with InfSet structure), iInf s ≤ a iff every lower bound b satisfying (∀ i, b ≤ s i) also satisfies b ≤ a.

Русский

Для семейства, индексированного по ι и принимающего значения в α (с структурой InfSet), iInf s ≤ a тогда и только тогда, когда любой нижний предел b, удовлетворяющий (∀ i, b ≤ s i), удовлетворяет b ≤ a.

LaTeX

$$$iInf s \le a \;\iff\; \forall b, (\forall i, b \le s i) \rightarrow b \le a$$$

Lean4

theorem iInf_le_iff {s : ι → α} : iInf s ≤ a ↔ ∀ b, (∀ i, b ≤ s i) → b ≤ a := by simp [iInf, sInf_le_iff, lowerBounds]

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