English
The distance between two extended maps is the maximum of the distance between their restrictions and the distance between their second components on the complement of the range.
Русский
Расстояние между двумя расширениями равно макс. расстоянию между их первыми компонентами и расстоянию между их вторыми компонентами на дополнении образа.
LaTeX
$$$\\operatorname{dist}(g_1.\\text{extend } f h_1, g_2.\\text{extend } f h_2) = \\max\\big(\\operatorname{dist}(g_1,g_2),\\operatorname{dist}(h_1\\restriction (\\operatorname{range}(f))^{c},\\; h_2\\restriction (\\operatorname{range}(f))^{c})\\big)$$$
Lean4
@[simp]
theorem dist_extend_extend (f : α ↪ δ) (g₁ g₂ : α →ᵇ β) (h₁ h₂ : δ →ᵇ β) :
dist (g₁.extend f h₁) (g₂.extend f h₂) =
max (dist g₁ g₂) (dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ)) :=
by
refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)
· rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
· simp only [extend_apply]
exact (dist_coe_le_dist x).trans (le_max_left _ _)
· simp only [extend_apply' hx]
lift x to ((range f)ᶜ : Set δ) using hx
calc
dist (h₁ x) (h₂ x) = dist (h₁.restrict (range f)ᶜ x) (h₂.restrict (range f)ᶜ x) := rfl
_ ≤ dist (h₁.restrict (range f)ᶜ) (h₂.restrict (range f)ᶜ) := (dist_coe_le_dist x)
_ ≤ _ := le_max_right _ _
· refine (dist_le dist_nonneg).2 fun x => ?_
rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
exact dist_coe_le_dist _
· refine (dist_le dist_nonneg).2 fun x => ?_
calc
dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
_ ≤ _ := dist_coe_le_dist _
