English
If f maps s1 to t1 bijectively and maps s2 to t2 bijectively and f is injective on s1 ∪ s2, then f induces a bijection 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)\\;\\land\\;\\text{BijOn}(f,s_2,t_2)\\;\\land\\;\\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_bijOn (h₁ : MapsTo f s₁ t₁) (h₂ : BijOn f s₂ t₂) (h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁) :
BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
inter_comm s₂ s₁ ▸ inter_comm t₂ t₁ ▸ h₂.inter_mapsTo h₁ h₃
