toRealizer

Mathlib.Data.Analysis.Topology

URI: https://scilib.ai/kg/mathlib#Ctop.toRealizer

← MathLib Explorer

English

Characterizes nhds membership via the realizer of the Ctop.

Русский

Характеризует принадлежность к nhds через реализатор Ctop.

LaTeX

$$$s \\in nhds a \\iff \\exists b, a \\in F.F b ∧ F.F b ⊆ s$$$

Lean4

/-- A `Ctop` realizes the topological space it generates. -/
protected def toRealizer (F : Ctop α σ) : @Ctop.Realizer _ F.toTopsp :=
  @Ctop.Realizer.mk _ F.toTopsp σ F rfl

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

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

Разделы

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

Аффилиация

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