ball_mono

Mathlib.Topology.UniformSpace.Defs

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

English

If V ⊆ W, then ball x V ⊆ ball x W.

Русский

Если V ⊆ W, то ball x V ⊆ ball x W.

LaTeX

$$$$V \\subseteq W \\Rightarrow ball\\ x\\ V \\subseteq ball\\ x\\ W.$$$$

Lean4

theorem ball_mono {V W : Set (β × β)} (h : V ⊆ W) (x : β) : ball x V ⊆ ball x W :=
  preimage_mono h

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

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

Разделы

Аффилиация

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