le_sup

Mathlib.Topology.MetricSpace.BundledFun

URI: https://scilib.ai/kg/mathlib#PseudoMetric.IsUltra.le_sup

English

In an ultrametric space, for any x,y,z, d(x,z) ≤ max{d(x,y), d(y,z)}.

Русский

В ультраметрическом пространстве для любых x,y,z выполняется неравенство: d(x,z) ≤ max{d(x,y), d(y,z)}.

LaTeX

$$$d(x,z) \le \max\{d(x,y), d(y,z)\}$.$$

Lean4

theorem le_sup [Zero R] [Add R] [LE R] [Max R] {d : PseudoMetric X R} [hd : IsUltra d] {x y z : X} :
    d x z ≤ d x y ⊔ d y z :=
  hd.le_sup' x y z

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru