sInter_eq_iInter — Mathlib

English

The intersection of a collection of sets equals the intersection over elements of a subtype: ⋂₀ s = ⋂ i : s, i.

Русский

Пересечение множества подмножеств равно пересечению элементов подсета: ⋂₀ s = ⋂_{i ∈ S} i.

LaTeX

$$$$ \\bigcap_{s \\in S} s = \\bigcap_{i \\in S} i. $$$$

Lean4

theorem sInter_eq_iInter {s : Set (Set α)} : ⋂₀ s = ⋂ i : s, i := by simp only [← sInter_range, Subtype.range_coe]

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