English
Let s_i be a directed family of subsets of A, f restricts to bijections from each s_i onto t_i, and the union is injective under f. Then f maps the intersection of all s_i bijectively onto the intersection of all t_i.
Русский
Пусть {s_i} образуют направленное семейство подмножеств A, ограничение f на каждый s_i даёт биекции f(s_i) = t_i, и f инъективна на объединении ⋃_i s_i. Тогда f отображает пересечение ⋂_i s_i биективно на ⋂_i t_i.
LaTeX
$$$[\text{hi}] \text{Nonempty } \iota\; \rightarrow \; (\forall i, \text{BijOn}(f, s_i, t_i)) \rightarrow \text{InjOn}(f, \bigcup_i s_i) \rightarrow \text{BijOn}(f, \bigcap_i s_i, \bigcap_i t_i)$$$
Lean4
theorem bijOn_iInter [hi : Nonempty ι] {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_iInter_iInter fun i => (H i).mapsTo, hi.elim fun i => (H i).injOn.mono (iInter_subset _ _),
surjOn_iInter_iInter (fun i => (H i).surjOn) Hinj⟩
