sInter_insert — Mathlib

English

Let s be a subset of α and T a collection of subsets of α. The intersection over insert s T equals s ∩ ⋂₀T: ⋂₀ insert s T = s ∩ ⋂₀T.

Русский

Пусть s ⊆ α и T — коллекция подмножеств α. Пересечение над вставкой s в T равно s ∩ ⋂₀T: ⋂₀ insert s T = s ∩ ⋂₀T.

LaTeX

$$$$ \\bigcap_{U \\in \\mathrm{insert}(s,T)} U = s \\cap \\big( \\bigcap_{V \\in T} V \\big). $$$$

Lean4

@[simp]
theorem sInter_insert (s : Set α) (T : Set (Set α)) : ⋂₀ insert s T = s ∩ ⋂₀ T :=
  sInf_insert

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