mono

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#ClusterPt.mono

English

If x is a cluster point of f ⊓ g, then x is a cluster point of f.

Русский

Если x — кластерная точка фильтра f ⊓ g, то x — кластерная точка фильтра f.

LaTeX

$$$\\mathrm{ClusterPt}(x, f\\cap g) \\Rightarrow \\mathrm{ClusterPt}(x,f)$$$

Lean4

theorem mono {f g : Filter X} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g :=
  NeBot.mono H <| inf_le_inf_left _ h

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

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

Разделы

Аффилиация

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