coe_eq_zero — Mathlib

English

For any a in the closed unit ball around 0, its image in 𝕜 is 0 if and only if a equals 0 in the ball.

Русский

Для любого a из закртого шара единицы вокруг 0 образ a в 𝕜 равен 0 тогда и только тогда, когда a = 0 в шаре.

LaTeX

$$$ (a : 𝕜) = 0 \iff a = 0$$$

Lean4

@[simp, norm_cast]
protected theorem coe_eq_zero [Zero 𝕜] [PseudoMetricSpace 𝕜] {a : closedBall (0 : 𝕜) 1} : (a : 𝕜) = 0 ↔ a = 0 :=
  Subtype.val_injective.eq_iff' unitClosedBall.coe_zero

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