mem_of_closed

Mathlib.Topology.Neighborhoods

URI: https://scilib.ai/kg/mathlib#Filter.Frequently.mem_of_closed

English

If s is closed and x is a limit point of s (i.e., x is frequently in nhds x ∩ s), then x ∈ s.

Русский

Если s замкнуто и x является пределом множества s, то x ∈ s.

LaTeX

$$IsClosed(s) ∧ x ∈ \\overline{s} ⇒ x ∈ s$$

Lean4

theorem mem_of_closed (h : ∃ᶠ x in 𝓝 x, x ∈ s) (hs : IsClosed s) : x ∈ s :=
  hs.closure_subset h.mem_closure

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

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

Разделы

Аффилиация

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