English
Let C be a collection of subsets of α, and for each s ∈ C a surjective map f_s : β → s (viewed as a subset of α). Then the union over β of the ranges of (f_s(y)).val across s equals the union of all members in C.
Русский
Пусть C — множество подмножеств α, и для каждого s ∈ C задано сюръекции f_s : β → s. Тогда ⋃_{y∈β} range((f_s y).val) = ⋃ C.
LaTeX
$$$$ \bigcup_{y \in \beta} \operatorname{range}\big(\lambda s : C, (f s y).\mathrm{val}\big) = \bigcup C $$$$
Lean4
theorem iUnion_range_eq_sUnion {α β : Type*} (C : Set (Set α)) {f : ∀ s : C, β → (s : Type _)}
(hf : ∀ s : C, Surjective (f s)) : ⋃ y : β, range (fun s : C => (f s y).val) = ⋃₀ C :=
by
ext x; constructor
· rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
refine ⟨_, hs, ?_⟩
exact (f ⟨s, hs⟩ y).2
· rintro ⟨s, hs, hx⟩
obtain ⟨y, hy⟩ := hf ⟨s, hs⟩ ⟨x, hx⟩
refine ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, ?_⟩
exact congr_arg Subtype.val hy
