subset_iInter₂_iff — Mathlib

English

For a family s(i)(j) of subsets, s ⊆ ⋂_i ⋂_j t(i)(j) holds iff ∀ i, ∀ j, s ⊆ t(i)(j).

Русский

Для семейства s(i)(j) верно, что s ⊆ ⋂_i ⋂_j t(i)(j) тогда и только тогда, когда для всех i и j верно s ⊆ t(i)(j).

LaTeX

$$$s \subseteq \bigcap_{i} \bigcap_{j} t_{ij} \iff \forall i, \forall j,\ s \subseteq t_{ij}$$$

Lean4

theorem subset_iInter₂_iff {s : Set α} {t : ∀ i, κ i → Set α} : (s ⊆ ⋂ (i) (j), t i j) ↔ ∀ i j, s ⊆ t i j := by
  simp_rw [subset_iInter_iff]

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