English
If each f_i is bijective from s_i to t_i and the t_i are pairwise disjoint, then hs.piecewise f is bijective.
Русский
Если каждый f_i биекции из s_i в t_i и t_i попарно не пересекаются, то hs.piecewise f биективна.
LaTeX
$$$\bigl(\forall i, \text{BijOn}(f_i, s_i, t_i)\bigr) \Rightarrow \text{Bijective}(hs.piecewise f)$$$
Lean4
/-- A family of bijective functions with pairwise disjoint
domains and pairwise disjoint ranges can be glued together
to form a bijective function. -/
theorem piecewise_bij {β : Type*} {f : ι → α → β} {t : ι → Set β} (ht : IndexedPartition t)
(hf : ∀ i, BijOn (f i) (s i) (t i)) : Bijective (piecewise hs f) :=
by
set g := piecewise hs f with hg
have hg_bij : ∀ i, BijOn g (s i) (t i) := by
intro i
refine BijOn.congr (hf i) ?_
intro x hx
rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]
have hg_inj : InjOn g (⋃ i, s i) := by
refine injOn_of_injective ?_
refine piecewise_inj hs (fun i ↦ BijOn.injOn (hf i)) ?h_disjoint
simp only [fun i ↦ BijOn.image_eq (hf i)]
rintro i - j - hij
exact ht.disjoint hij
rw [bijective_iff_bijOn_univ, ← hs.iUnion, ← ht.iUnion]
exact bijOn_iUnion hg_bij hg_inj
