iUnion_iUnion_eq' — Mathlib

English

Let f : ι → α and g : α → Set β. Then ∪_{x} ∪_{y} (f y = x) ∧ g x equals ∪_{y} g(f y).

Русский

Пусть f: ι → α, g: α → Set β. Тогда объединение по парам (x,y) с условием f(y)=x от g(x) равно объединению по y: g(f(y)).

LaTeX

$$$\bigcup_{x} \bigcup_{y: f(y)=x} g(x) = \bigcup_{y} g(f(y))$$$

Lean4

@[simp]
theorem iUnion_iUnion_eq' {f : ι → α} {g : α → Set β} : ⋃ (x) (y) (_ : f y = x), g x = ⋃ y, g (f y) := by
  simpa using biUnion_range

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