English
Let {s_i} be subsets of A and {t_i} be subsets of B, and f: A → B. If for every i the restriction of f to s_i is onto t_i and f is injective on the union of all s_i, then f maps the intersection of all s_i onto the intersection of all t_i.
Русский
Пусть {s_i} — подмножества A, {t_i} — подмножества B, и f: A → B. Если для каждого i отображение f ограниченного на s_i достигает t_i и функция f инъективна на объединении всех s_i, то отображение f ограниченное на пересечение ⋂_i s_i отображаеться на ⋂_i t_i.
LaTeX
$$$\left(\forall i, f[s_i] = t_i\right) \wedge \operatorname{InjOn}(f, \bigcup_i s_i) \Rightarrow f\bigl(\bigcap_i s_i\bigr) = \bigcap_i t_i$$$
Lean4
theorem surjOn_iInter_iInter [Nonempty ι] {s : ι → Set α} {t : ι → Set β} {f : α → β} (H : ∀ i, SurjOn f (s i) (t i))
(Hinj : InjOn f (⋃ i, s i)) : SurjOn f (⋂ i, s i) (⋂ i, t i) :=
surjOn_iInter (fun i => (H i).mono (Subset.refl _) (iInter_subset _ _)) Hinj
