iInf₂_eq_bot — Mathlib

English

Let f: ∀ i, κ i → α be a family of elements in a complete linear order. The infimum over i and j of f(i,j) equals ⊥ if and only if for every b > ⊥ there exist i and j with f(i,j) < b.

Русский

Пусть f: ∀ i, κ i → α. Инфинум по i и j равен ⊥ тогда и только тогда, когда для каждого b > ⊥ существуют i и j, такие что f(i,j) < b.

LaTeX

$$$\\displaystyle \\inf_{i} \\inf_{j} f(i,j) = ⊥ \\iff \\forall b > ⊥, \\exists i, \\exists j, f(i,j) < b$$$

Lean4

theorem iInf₂_eq_bot (f : ∀ i, κ i → α) : ⨅ i, ⨅ j, f i j = ⊥ ↔ ∀ b > ⊥, ∃ i j, f i j < b := by
  simp_rw [iInf_psigma', iInf_eq_bot, PSigma.exists]

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