English
A family {f_i} of injective functions with pairwise disjoint domains and pairwise disjoint images yields an injective piecewise function.
Русский
Семейство функций {f_i} с попарно разложенными на множества доменами и попарно раздельными образами порождает инъективную кусочную функцию.
LaTeX
$$$(\forall i, \mathrm{InjOn}(f_i, s_i)) \land (\mathrm{PairwiseDisjoint} (univ : \mathrm{Set} \ ι) (\lambda i, (f_i)''(s_i))) \Rightarrow \mathrm{Injective}(hs.piecewise f)$$$
Lean4
/-- A family of injective functions with pairwise disjoint
domains and pairwise disjoint ranges can be glued together
to form an injective function. -/
theorem piecewise_inj {β : Type*} {f : ι → α → β} (h_injOn : ∀ i, InjOn (f i) (s i))
(h_disjoint : PairwiseDisjoint (univ : Set ι) fun i => (f i) '' (s i)) : Injective (piecewise hs f) :=
by
intro x y h
suffices hs.index x = hs.index y
by
apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)
simpa only [piecewise_apply, this] using h
apply h_disjoint.elim trivial trivial
contrapose! h
exact h.ne_of_mem (mem_image_of_mem _ (hs.mem_index x)) (mem_image_of_mem _ (hs.mem_index y))
