biInter_insert — Mathlib

English

Let a ∈ α, s ⊆ α, and t : α → Set β. The intersection over x ∈ insert a s of t(x) equals t(a) ∩ ⋂ x ∈ s, t(x).

Русский

Пусть a ∈ α, s ⊆ α, и t : α → Set β. Пересечение по x ∈ insert(a,s) t(x) равно t(a) ∩ ⋂_{x ∈ s} t(x).

LaTeX

$$$\\\\bigcap_{x \\in insert(a, s)} t(x) = t(a) \\cap \\\\bigcap_{x \\in s} t(x)$$$

Lean4

theorem biInter_insert (a : α) (s : Set α) (t : α → Set β) : ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x := by simp

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