mem_iSup₂_iff — Mathlib

English

For a family f : ∀ i, κ i → UpperSet α, a ∈ ⨆ (i) (j), f i j if and only if ∀ i ∀ j, a ∈ f i j.

Русский

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

LaTeX

$$$ a \in \bigvee_{i} \bigl( f_i \bigr) \;?\; \text{ (вложенный индекс)} $$$

Lean4

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

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