English
If f is bijective on s1 to t1 and on s2 to t2, and f is injective on the union s1 ∪ s2, then f is bijective on s1 ∩ s2 to t1 ∩ t2.
Русский
Если f биекция на s1→t1 и на s2→t2, и f инъективна на s1 ∪ s2, то f биекция на s1 ∩ s2 → t1 ∩ t2.
LaTeX
$$$\\text{BijOn}(f,s_1,t_1)\\to\\text{BijOn}(f,s_2,t_2)\\to\\text{InjOn}(f,(s_1\\cup s_2))\\Rightarrow\\text{BijOn}(f,(s_1\\cap s_2),(t_1\\cap t_2))$$$
Lean4
theorem inter (h₁ : BijOn f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h : InjOn f (s₁ ∪ s₂)) : BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
⟨h₁.mapsTo.inter_inter h₂.mapsTo, h₁.injOn.mono inter_subset_left, h₁.surjOn.inter_inter h₂.surjOn h⟩
