English
A neighborhood realizer of a point a is obtained from F by restricting to those indices s with a ∈ F.F s, and transporting the associated data to form a local neighborhood realizer at a.
Русский
Реализатор окрестности точки a получается из F путём ограничения по тем индексам s, для которых a ∈ F.F s, и переноса соответствующих данных в реализатор окрестности в a.
LaTeX
$$$ (F\mathrm{nhds}\ a) = \langle \{ s : F.\sigma \mid a \in F.F s \}, \; \dots \rangle $$$$
Lean4
/-- A realizer of the neighborhood of a point. -/
protected def nhds (F : Realizer α) (a : α) : (𝓝 a).Realizer :=
⟨{ s : F.σ // a ∈ F.F s },
{ f := fun s ↦ F.F s.1
pt := ⟨_, F.F.top_mem a⟩
inf := fun ⟨x, h₁⟩ ⟨y, h₂⟩ ↦ ⟨_, F.F.inter_mem x y a ⟨h₁, h₂⟩⟩
inf_le_left := fun ⟨x, h₁⟩ ⟨y, h₂⟩ _z h ↦ (F.F.inter_sub x y a ⟨h₁, h₂⟩ h).1
inf_le_right := fun ⟨x, h₁⟩ ⟨y, h₂⟩ _z h ↦ (F.F.inter_sub x y a ⟨h₁, h₂⟩ h).2 },
filter_eq <|
Set.ext fun _x ↦
⟨fun ⟨⟨_s, as⟩, h⟩ ↦ mem_nhds_iff.2 ⟨_, h, F.isOpen _, as⟩, fun h ↦
let ⟨s, h, as⟩ := F.mem_nhds.1 h
⟨⟨s, h⟩, as⟩⟩⟩
