coe_zero — Mathlib

English

Let 𝕜 be a type with a zero and a pseudometric space. The zero element of the closed unit ball around 0 is mapped to 0 in 𝕜 by the canonical inclusion.

Русский

Пусть 𝕜 — тип с нулём и псевдометрическим пространством. Замкнутый шар единицы вокруг нуля, как подмножество 𝕜, вкладывается в 𝕜 так, что ноль шара отображается в ноль в 𝕜.

LaTeX

$$$((0 : \\overline{B}(0,1)) : 𝕜) = 0$$$

Lean4

@[simp, norm_cast]
protected theorem coe_zero [Zero 𝕜] [PseudoMetricSpace 𝕜] : ((0 : closedBall (0 : 𝕜) 1) : 𝕜) = 0 :=
  rfl

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