ball_inter_right

Mathlib.Topology.UniformSpace.Defs

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

English

If you take the ball around x with V ∩ W, it is contained in the ball around x with W.

Русский

Если взять шар вокруг x ради V ∩ W, он содержится в шаре вокруг x ради W.

LaTeX

$$$\operatorname{ball}(x, V \cap W) \subseteq \operatorname{ball}(x, W)$$$

Lean4

theorem ball_inter_right (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x W :=
  ball_mono inter_subset_right x

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

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

Разделы

Аффилиация

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