isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm

English

If for all x,y in S' we have ‖x·y‖₊ ≤ max(‖x‖₊, ‖y‖₊), then IsUltrametricDist S'.

Русский

Если для всех x,y в S' выполняется ‖x·y‖₊ ≤ max(‖x‖₊, ‖y‖₊), то S' имеет ультраметрическое расстояние.

LaTeX

$$$\\Big(\\forall x,y \\in S',\\ ‖x y‖_+ ≤ \\max(‖x‖_+, ‖y‖_+)\\Big) \\implies \\mathrm{IsUltrametricDist}(S')$$$

Lean4

@[to_additive]
theorem isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm (h : ∀ x y : S', ‖x * y‖₊ ≤ max ‖x‖₊ ‖y‖₊) :
    IsUltrametricDist S' :=
  isUltrametricDist_of_forall_norm_mul_le_max_norm h

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