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]