coe_unitBall_apply_zero — Mathlib

English

The unitBall homeomorphism sends the origin to the origin; that is, H(0) = 0 where H is the unitBall.

Русский

Гомеоморфизм единичного шара отправляет нуль в нуль; то есть H(0) = 0, где H — гомеоморфизм единичного шара.

LaTeX

$$$H(0) = 0,$ где $H: E \cong \mathrm{ball}(0,1)$ — соответствующий гомеоморфизм.$$

Lean4

@[simp]
theorem coe_unitBall_apply_zero : (Homeomorph.unitBall (0 : E) : E) = 0 :=
  OpenPartialHomeomorph.univUnitBall_apply_zero

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