English
The concatenation map Path.trans: Path x y → Path y z → Path x z is uniformly continuous in both arguments jointly.
Русский
Соединение Path.trans: Path x y → Path y z → Path x z равномерно непрерывно по обоим аргументам одновременно.
LaTeX
$$$\text{UniformContinuous}(\mathrm{Path}.\mathrm{trans}).\ uncurry$$$
Lean4
/-- The function `Path.trans` that concatenates two paths `γ₁ : Path x y` and `γ₂ : Path y z`
is uniformly continuous in `(γ₁, γ₂)`. -/
theorem uniformContinuous_trans : UniformContinuous (Path.trans : Path x y → Path y z → Path x z).uncurry :=
hasBasis_uniformity.uniformity_prod hasBasis_uniformity |>.uniformContinuous_iff hasBasis_uniformity |>.mpr fun U hU ↦
⟨(U, U), ⟨hU, hU⟩, fun ⟨_, _⟩ ⟨_, _⟩ ⟨h₁, h₂⟩ t ↦ by
by_cases ht : (t : ℝ) ≤ 2⁻¹ <;> simp [Path.trans_apply, ht, h₁ _, h₂ _]⟩
