mem_iSup₂_iff — Mathlib

English

Let f(i, j) be a family of lower sets indexed by i and j. Then a ∈ ⨆ (i) (j), f i j if and only if there exist i and j with a ∈ f(i, j).

Русский

Пусть f(i, j) — семейство нижних множеств, индексируемое i и j. Тогда a ∈ ⨆_{i,j} f(i,j) тогда и только тогда, когда существуют i и j, такие что a ∈ f(i, j).

LaTeX

$$$a \in \bigvee_{i}\bigvee_{j} f(i,j) \iff \exists i \exists j, a \in f(i,j)$$$

Lean4

theorem mem_iSup₂_iff {f : ∀ i, κ i → LowerSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j := by simp

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