English
If s1 ⊥ s2 (disjoint), then InjOn f (s1 ∪ s2) is equivalent to InjOn f s1, InjOn f s2, and non-equality across the two parts.
Русский
Если s1 и s2 различны и непересекаются, то InjOn f (s1 ∪ s2) эквивалентно InjOn f s1, InjOn f s2 и условию, что значения f на s1 и s2 различаются.
LaTeX
$$$\\\\Disjoint s_1 s_2 \\\\rightarrow \\\\Big( InjOn f (s_1 \\\\cup s_2) \\\\Leftrightarrow (InjOn f s_1 \\\\land InjOn f s_2 \\\\land \\\\forall x \\\\in s_1, \\\\forall y \\\\in s_2, f x \\\\neq f y)) \\\\Big)$$$
Lean4
theorem injOn_union (h : Disjoint s₁ s₂) :
InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y :=
by
refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩
· intro x hx y hy hxy
obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
exact h.le_bot ⟨hx, hy⟩
· rintro ⟨h₁, h₂, h₁₂⟩
rintro x (hx | hx) y (hy | hy) hxy
exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]
