univUnitBall_apply_zero

Mathlib.Analysis.Normed.Module.Ball.Homeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.univUnitBall_apply_zero

English

Applying the unit-ball map to zero yields zero, i.e., f(0) = 0.

Русский

Применение отображения единичного шара к нулю даёт ноль: f(0) = 0.

LaTeX

$$$f(0)=0$ where $f=\text{univUnitBall}$$$

Lean4

@[simp]
theorem univUnitBall_apply_zero : univUnitBall (0 : E) = 0 := by simp [OpenPartialHomeomorph.univUnitBall_apply]

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

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

Разделы

Аффилиация

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