English
If ι is nonempty, s_i form a directed family of subsets of A, and each f restricted to s_i is a bijection onto t_i, then f maps the intersection of all s_i bijectively onto the intersection of all t_i.
Русский
Пусть ι непусто, {s_i} образует направленное семейство подмножеств A, и для каждого i отображение f ограничено на s_i даёт биективное отображение на t_i. Тогда f отображает пересечение ⋂_i s_i биективно на ⋂_i t_i.
LaTeX
$$$[\text{hi}] \; (\forall i, \BijOn f (s_i) (t_i)) \rightarrow \InjOn f (\bigcup_i s_i) \rightarrow \BijOn f (\bigcap_i s_i) (\bigcap_i t_i)$$$
Lean4
theorem bijOn_iInter_of_directed [Nonempty ι] {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_iInter H <| inj_on_iUnion_of_directed hs fun i => (H i).injOn
