of_inf_left

Mathlib.Topology.ClusterPt

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_inf_left {f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x f :=
  H.mono inf_le_left

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

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

Разделы

Аффилиация

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