mem_nhds — Mathlib

English

Extends mem_nhds characterization to arbitrary TopologicalSpace via equality of realizers.

Русский

Расширяет характеристику mem_nhds до произвольного TopologicalSpace через равенство реализаторов.

LaTeX

$$$\\text{mem\_nhds}(F) = \\text{mem\_nhds\_toTopsp}(F)$$$

Lean4

protected theorem mem_nhds [T : TopologicalSpace α] (F : Realizer α) {s : Set α} {a : α} :
    s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F b ∧ F.F b ⊆ s := by have := @mem_nhds_toTopsp _ _ F.F s a; rwa [F.eq] at this

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