English
For a bounded scalar action, the distance between x•y1 and x•y2 is bounded by dist x 0 times dist(y1,y2).
Русский
Для ограниченного действия скаляра расстояние между x·y1 и x·y2 не превосходит расстояния x от 0, умноженное на расстояние y1,y2.
LaTeX
$$dist(x•y1, x•y2) ≤ dist(x,0) · dist(y1,y2)$$
Lean4
/-- The typeclass `IsBoundedSMul` on a metric-space scalar action implies continuity of the
action. -/
instance (priority := 100) continuousSMul : ContinuousSMul α β where
continuous_smul := by
rw [Metric.continuous_iff]
rintro ⟨a, b⟩ ε ε0
obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε :=
by
have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by fun_prop
refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt
simp
refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩
obtain ⟨ha, hb⟩ := max_lt_iff.1 hab'
calc
dist (a' • b') (a • b) ≤ dist (a' • b') (a • b') + dist (a • b') (a • b) := dist_triangle ..
_ ≤ dist a' a * dist b' 0 + dist a 0 * dist b' b := (add_le_add (dist_pair_smul _ _ _) (dist_smul_pair _ _ _))
_ ≤ δ * (δ + dist b 0) + dist a 0 * δ :=
by
have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
gcongr
_ < ε := hδε
