emetric_ball_top

Mathlib.Topology.MetricSpace.Pseudo.Defs

URI: https://scilib.ai/kg/mathlib#Metric.emetric_ball_top

English

The open ball with the top radius equals the entire space: EMetric.ball x ⊤ = univ.

Русский

Открытый шар с верхним радиусом равен всего пространству: EMetric.ball x ⊤ = единица пространства.

LaTeX

$$$\\forall x\\in α,\\ EMetric.ball x \\top = \\mathrm{univ}$.$$

Lean4

@[simp]
theorem emetric_ball_top (x : α) : EMetric.ball x ⊤ = univ :=
  eq_univ_of_forall fun _ => edist_lt_top _ _

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

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

Разделы

Аффилиация

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