sUnion_range — Mathlib

English

Let f be a function from ι to subsets of β. The union over the range of f equals the union over all x of f(x): ⋃₀ range f = ⋃ x, f x.

Русский

Пусть f: ι → Set β. Объединение над охватом функции равно объединению по всем x: ⋃₀ range f = ⋃ x, f x.

LaTeX

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

Lean4

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

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