isUltrametricDist_of_forall_norm_mul_le_max_norm

English

Let S' be a seminormed group such that for all x, y in S', ‖x · y‖ ≤ max(‖x‖, ‖y‖). Then the induced metric d(x, y) = ‖x⁻¹ y‖ (or equivalently dist(x, y)) is ultrametric on S'.

Русский

Пусть S' — полугруппа с нормой так, что для всех x, y в S' выполнено ‖x · y‖ ≤ max(‖x‖, ‖y‖). Тогда индуцированная метрика d(x, y) = ‖x⁻¹ y‖ (или dist(x, y)) образует ультраметрическое пространство на S'.

LaTeX

$$$\\Big(\\forall x,y \\in S',\\ \\|xy\\| \\le \\max(\\|x\\|, \\|y\\|)\\Big) \\implies \\mathrm{IsUltrametricDist}(S')$$$

Lean4

@[to_additive]
theorem isUltrametricDist_of_forall_norm_mul_le_max_norm (h : ∀ x y : S', ‖x * y‖ ≤ max ‖x‖ ‖y‖) : IsUltrametricDist S'
    where
  dist_triangle_max x y z := by simpa only [dist_eq_norm_div, le_max_iff, div_mul_div_cancel] using h (x / y) (y / z)

Похожие утверждения