instInhabitedRealizer

Mathlib.Data.Analysis.Topology

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

English

Corollary form for mem_nhds_toTopsp expressed via equivalence under mk.

Русский

Корутина mem_nhds_toTopsp как эквивалентность относительно mk.

LaTeX

$$$\\text{mem\_nhds\_toTopsp}(F)(s,a) = \\exists b, a \\in F.F b ∧ F.F b ⊆ s$$$

Lean4

instance (F : Ctop α σ) : Inhabited (@Ctop.Realizer _ F.toTopsp) :=
  ⟨F.toRealizer⟩

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

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

Разделы

Аффилиация

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