subset_ball

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#Bornology.IsBounded.subset_ball

English

If s is bounded, then for any center c there exists r with s ⊆ ball(c,r).

Русский

Если s ограничено, то для любого центра c существует r такой, что s ⊆ ball(c,r).

LaTeX

$$IsBounded(s) → ∀ c, ∃ r, s ⊆ ball c r$$

Lean4

theorem _root_.Bornology.IsBounded.subset_ball (h : IsBounded s) (c : α) : ∃ r, s ⊆ ball c r :=
  (h.subset_ball_lt 0 c).imp fun _ ↦ And.right

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

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

Разделы

Аффилиация

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