sInter_eq_biInter — Mathlib

English

The intersection of a collection of sets equals the intersection over its elements indexed by S: ⋂₀ s = ⋂ (i ∈ S), i.

Русский

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

LaTeX

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

Lean4

theorem sInter_eq_biInter {s : Set (Set α)} : ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i := by rw [← sInter_image, image_id']

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