insert_iInter — Mathlib

English

For any x and a family t_i of sets, inserting x into the intersection distributes: insert x (⋂_i t_i) = ⋂_i insert x (t_i).

Русский

Для любого x и семейства t_i верно: вставка x в пересечение распределяется: insert x (⋂_i t_i) = ⋂_i insert x (t_i).

LaTeX

$$$ \operatorname{insert}(x, \bigcap_i t_i) = \bigcap_i \operatorname{insert}(x, t_i) $$$

Lean4

theorem insert_iInter (x : β) (t : ι → Set β) : insert x (⋂ i, t i) = ⋂ i, insert x (t i) := by
  simp_rw [← union_singleton, iInter_union]

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