accPt_sup

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#accPt_sup

English

For any X and filters F, G, AccPt x (F ⊔ G) holds iff AccPt x F or AccPt x G holds.

Русский

Для любых X, фильтров F, G: AccPt x (F ⊔ G) эквивалентно AccPt x F или AccPt x G.

LaTeX

$$$\\mathrm{AccPt}(x, F \\sqcup G) \\iff \\mathrm{AccPt}(x,F) \\lor \\mathrm{AccPt}(x,G)$$$

Lean4

theorem accPt_sup {x : X} {F G : Filter X} : AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G := by
  simp only [AccPt, inf_sup_left, sup_neBot]

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

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

Разделы

Аффилиация

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