univBall_apply_zero

Mathlib.Analysis.Normed.Module.Ball.Homeomorph

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

English

For any c and r, the map univBall(c,r) sends 0 to c.

Русский

Отображение univBall(c,r) отправляет 0 в точку c.

LaTeX

$$$\mathrm{univBall}(c,r)(0) = c.$$$

Lean4

@[simp]
theorem univBall_apply_zero (c : P) (r : ℝ) : univBall c r 0 = c := by unfold univBall; split_ifs <;> simp

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

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

Разделы

Аффилиация

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