coe_bot

Mathlib.Topology.MetricSpace.BundledFun

URI: https://scilib.ai/kg/mathlib#PseudoMetric.coe_bot

English

The bottom metric coincides with the zero function: ⊥ = 0 as a function.

Русский

Нижняя метрика совпадает с нулевой функцией: ⊥ = 0 как функция.

LaTeX

$$$\bot = 0$ as a function, i.e. for all x,y, $(\bot)(x,y)=0$.$$

Lean4

@[simp, norm_cast]
theorem coe_bot [AddZeroClass R] [Preorder R] : ⇑(⊥ : PseudoMetric X R) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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