isClosed_ball

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#UniformSpace.isClosed_ball

English

If V is a closed set of α×α, then the ball x V is a closed set in α for any x ∈ α.

Русский

Если V замкнуто в α×α, то шар вокруг x по V замкнут в α.

LaTeX

$$$\\operatorname{IsClosed}(V) \\Rightarrow \\operatorname{IsClosed}(\\mathrm{ball}\\, x\\, V)$$$

Lean4

theorem isClosed_ball (x : α) {V : Set (α × α)} (hV : IsClosed V) : IsClosed (ball x V) :=
  hV.preimage <| .prodMk_right _

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

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

Разделы

Аффилиация

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