English
If f is bijective from s1 to t1 and maps s2 to t2, and if every element of s1 that maps into t2 already lies in s2, then f is bijective from s1 ∩ s2 onto t1 ∩ t2.
Русский
Если f является биекцией на s1→t1 и отображает s2 в t2, и если каждый элемент из s1, который образуется в t2, на самом деле принадлежит s2, тогда f задаёт биекцию на s1 ∩ s2 → t1 ∩ t2.
LaTeX
$$$\\bigl(\\text{BijOn}(f,s_1,t_1)\\bigr) \\land \\bigl(\\text{BijOn}(f,s_2,t_2)\\bigr) \\land \\bigl(\\text{InjOn}(f,(s_1\\cup s_2))\\bigr) \\Rightarrow \\text{BijOn}(f,(s_1\\cap s_2),(t_1\\cap t_2))$$
Lean4
theorem inter_mapsTo (h₁ : BijOn f s₁ t₁) (h₂ : MapsTo f s₂ t₂) (h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂) :
BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
⟨h₁.mapsTo.inter_inter h₂, h₁.injOn.mono inter_subset_left, fun _ hy =>
let ⟨x, hx, hxy⟩ := h₁.surjOn hy.1
⟨x, ⟨hx, h₃ ⟨hx, hxy.symm.subst hy.2⟩⟩, hxy⟩⟩
