nhds_nhdsAdjoint_same — Mathlib

English

The neighborhood filter of a in nhdsAdjoint(a,f) equals pure(a) ⊔ f.

Русский

Окрестностной фильтр в a для топологии nhdsAdjoint(a,f) равен чистому фильтру a ⊔ f.

LaTeX

$$@nhds α (nhdsAdjoint a f) a = pure a ⊔ f$$

Lean4

theorem nhds_nhdsAdjoint_same (a : α) (f : Filter α) : @nhds α (nhdsAdjoint a f) a = pure a ⊔ f :=
  by
  let _ := nhdsAdjoint a f
  apply le_antisymm
  · rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩
    exact IsOpen.mem_nhds (fun _ ↦ htf) hat
  · exact sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f)

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