mem_derivedSet

Mathlib.Topology.DerivedSet

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

English

x ∈ derivedSet A iff AccPt x (principal A).

Русский

x принадлежит производному множеству A тогда и только тогда, когда x — точка накопления множества A.

LaTeX

$$$$x \in \operatorname{derivedSet}(A) \iff \AccPt x (\operatorname{principal} A).$$$$

Lean4

@[simp]
theorem mem_derivedSet {A : Set X} {x : X} : x ∈ derivedSet A ↔ AccPt x (𝓟 A) :=
  Iff.rfl

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

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

Разделы

Аффилиация

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