frequently'

Mathlib.Topology.ClusterPt

URI: https://scilib.ai/kg/mathlib#ClusterPt.frequently'

← MathLib Explorer

English

frontier(s) = (interior(s))^c ∩ (interior(s^c))^c.

Русский

frontier(s) = (интерьер(s))^c ∩ (интерьер(s^c))^c.

LaTeX

$$$\\operatorname{frontier}(s) = (\\operatorname{interior}(s))^c \\cap (\\operatorname{interior}(s^c))^c$$$

Lean4

theorem frequently' {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ y in F, p y) : ∃ᶠ y in 𝓝 x, p y :=
  clusterPt_iff_frequently'.mp hx {y | p y} hp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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