English
If for each i ∈ ι there is a surjective f_i : β → C_i where C_i ⊆ α, then the union over β of the range of (f_i y).val across i equals the union over i of C_i.
Русский
Для каждого i ∈ ι имеется сюръекция f_i : β → C_i; тогда ⋃_{y} range((f_i y).val) = ⋃_{i} C_i.
LaTeX
$$$$ \bigcup_{y \in \beta} \operatorname{range}\big(\lambda i : ι, (f i y).\mathrm{val}\big) = \bigcup_{i \in ι} C_i $$$$
Lean4
theorem iUnion_range_eq_iUnion (C : ι → Set α) {f : ∀ x : ι, β → C x} (hf : ∀ x : ι, Surjective (f x)) :
⋃ y : β, range (fun x : ι => (f x y).val) = ⋃ x, C x :=
by
ext x; rw [mem_iUnion, mem_iUnion]; constructor
· rintro ⟨y, i, rfl⟩
exact ⟨i, (f i y).2⟩
· rintro ⟨i, hx⟩
obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
exact ⟨y, i, congr_arg Subtype.val hy⟩
