English
If the index system s_i is directed by inclusion and each f restricted to s_i is a bijection onto t_i, then f maps the union of all s_i bijectively onto the union of all t_i (provided the union is injective).
Русский
Если семейство индексов s_i упорядочено включением (направлено) и для каждого i отображение f ограничено на s_i даёт биекцию на t_i, то f отображает объединение ⋃_i s_i биективно на ⋃_i t_i (при условии инъективности на объединении).
LaTeX
$$$\bigl(\forall i, \BijOn f\ (s_i) (t_i)\bigr) \rightarrow \InjOn(f, \bigcup_i s_i) \rightarrow \BijOn f (\bigcup_i s_i) (\bigcup_i t_i)$$$
Lean4
theorem bijOn_iUnion_of_directed {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {t : ι → Set β} {f : α → β}
(H : ∀ i, BijOn f (s i) (t i)) : BijOn f (⋃ i, s i) (⋃ i, t i) :=
bijOn_iUnion H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn
