iInter₂_union — Mathlib

English

Let s ⊆ α and f : α → Set β. Then the intersection over i of f(i) equals the intersection over i ∈ s of f(⟨i, hi⟩).

Русский

Пусть s ⊆ α и f : α → Set β. Тогда пересечение по i f(i) равно пересечению по i ∈ s f(⟨i, hi⟩).

LaTeX

$$$\\\\bigcap_{i} f(i) = \\\\bigcap_{i \\in s} f(\\\\langle i, hi \\\\rangle)$$$

Lean4

theorem iInter₂_union (s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) ∪ t = ⋂ (i) (j), s i j ∪ t := by
  simp_rw [iInter_union]

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