iUnion₂_subset_iff — Mathlib

English

Let s(i)(j) be a family of subsets of α indexed by i and j. Then ⋃_i ⋃_j s(i)(j) ⊆ t if and only if ∀ i, ∀ j, s(i)(j) ⊆ t.

Русский

Пусть s(i)(j) — семейство подмножеств α, индексируемое по i и j. Тогда ⋃_i ⋃_j s(i)(j) ⊆ t тогда и только тогда, когда для всех i и j выполняется s(i)(j) ⊆ t.

LaTeX

$$$\bigcup_{i} \bigcup_{j} s_{ij} \subseteq t \iff \forall i, \forall j, s_{ij} \subseteq t$$$

Lean4

theorem iUnion₂_subset_iff {s : ∀ i, κ i → Set α} {t : Set α} : ⋃ (i) (j), s i j ⊆ t ↔ ∀ i j, s i j ⊆ t := by
  simp_rw [iUnion_subset_iff]

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