sInter_range — Mathlib

English

Let f be a function ι → Set β. The intersection over the range of f equals the intersection over x of f(x): ⋂₀ range f = ⋂ x, f x.

Русский

Пусть f: ι → Set β. Пересечение над диапазоном f равно пересечению по всем x: ⋂₀ range f = ⋂ x, f x.

LaTeX

$$$$ \\bigcap_{U \\in \\mathrm{range}(f)} U = \\bigcap_{x} f(x). $$$$

Lean4

@[simp]
theorem sInter_range (f : ι → Set β) : ⋂₀ range f = ⋂ x, f x :=
  rfl

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