English
Piecewise injective construction: if f, f' are injective and outputs are separated, the resulting piecewise function is injective.
Русский
Разделённая по условию конструкция сохраняет инъективность при раздельной аппроксимации значений.
LaTeX
$$∀{α,β,γ}, (p: α → Prop) → [DecidablePred p] → (f: {a:α // p a} → β) → (f': {a:α // ¬p a} → β) → Injective f → Injective f' → (∀{x x'}, hx: p x, hx': ¬p x', f ⟨x,hx⟩ ≠ f' ⟨x',hx'⟩) → Injective (λ x => if h : p x then f ⟨x,h⟩ else f' ⟨x,h⟩)$$
Lean4
theorem dite (p : α → Prop) [DecidablePred p] {f : { a : α // p a } → β} {f' : { a : α // ¬p a } → β} (hf : Injective f)
(hf' : Injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) :
Function.Injective (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) := fun x₁ x₂ h =>
by
dsimp only at h
by_cases h₁ : p x₁ <;> by_cases h₂ : p x₂
· rw [dif_pos h₁, dif_pos h₂] at h; injection (hf h)
· rw [dif_pos h₁, dif_neg h₂] at h; exact (im_disj h).elim
· rw [dif_neg h₁, dif_pos h₂] at h; exact (im_disj h.symm).elim
· rw [dif_neg h₁, dif_neg h₂] at h; injection (hf' h)
