English
Let f: A → B and {s_i} ⊆ A, {t_i} ⊆ B be such that for every i, f restricts to a bijection from s_i onto t_i, and f is injective on ⋃_i s_i. Then f maps ⋃_i s_i bijectively onto ⋃_i t_i.
Русский
Пусть f: A → B и {s_i} ⊆ A, {t_i} ⊆ B таковы, что для каждого i ограничение f на s_i является биекцией на t_i, и f инъективна на ⋃_i s_i. Тогда f отображает ⋃_i s_i биективно на ⋃_i t_i.
LaTeX
$$$\bigl(\forall i, \text{BijOn}(f, s_i, t_i)\bigr) \rightarrow \operatorname{InjOn}(f, \bigcup_i s_i) \rightarrow \operatorname{BijOn}(f, \bigcup_i s_i, \bigcup_i t_i)$$$
Lean4
theorem bijOn_iUnion {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, BijOn f (s i) (t i))
(Hinj : InjOn f (⋃ i, s i)) : BijOn f (⋃ i, s i) (⋃ i, t i) :=
⟨mapsTo_iUnion_iUnion fun i => (H i).mapsTo, Hinj, surjOn_iUnion_iUnion fun i => (H i).surjOn⟩
