English
The piecewise function s.piecewise f g is injective iff f is injective on s, g is injective on sᶜ, and no collision occurs between f on s and g on sᶜ for elements from s and its complement.
Русский
Кусочно-заданная функция s.piecewise f g инъективна тогда и только тогда, когда f инъективна на s, g инъективна на sᶜ и не возникает совпадения между значениями на s и на sᶜ для элементов из s и его дополнения.
LaTeX
$$$\\operatorname{Injective}(s.piecewise f g) \\iff InjOn f s \\land InjOn g s^{c} \\land \\forall x \\in s, \\forall y \\notin s, f x \\neq g y$$$
Lean4
theorem injective_piecewise_iff {f g : α → β} :
Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y :=
by
rw [injective_iff_injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
(piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_notMem s f g hy]
