coe_eq_zero — Mathlib

English

For any a in the unit ball, a maps to zero in 𝕜 if and only if a is the zero element of the unit ball.

Русский

Для любого a в единичной сфере отображение a в 𝕜 равно нулю тогда и только тогда, когда a = 0 в единичной сфере.

LaTeX

$$$\\forall a \\in \\text{ball}(0,1),\\; a = 0 \\iff a = 0_{ball}$$$

Lean4

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

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