mem_iInf₂_iff — Mathlib

English

For a family f : ∀ i, κ i → UpperSet α, a ∈ ⨅ (i) (j), f i j iff ∃ i ∃ j, a ∈ f i j.

Русский

Для семейства f i j верно: a ∈ ⨅ i j f i j тогда, когда существует пара индексов (i,j) с a ∈ f i j.

LaTeX

$$$ a \in \bigwedge (i) (j), f i j \iff \exists i \exists j, a \in f i j $$$

Lean4

theorem mem_iInf₂_iff {f : ∀ i, κ i → UpperSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j := by simp

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