ball_inter_left

Mathlib.Topology.UniformSpace.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem ball_inter_left (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x V :=
  ball_mono inter_subset_left x

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

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

Разделы

Аффилиация

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