nhds_nhdsAdjoint — Mathlib

English

If α has decidable equality, the nhds of nhdsAdjoint(a,f) equals an update of the pure filter at a by sup with f.

Русский

При наличии дизъюнктивного равенства для α, окрестностной фильтр nhdsAdjoint(a,f) равен обновлению чистого фильтра в a, объединённому с f.

LaTeX

$$theorem nhds_nhdsAdjoint [DecidableEq α] (a : α) (f : Filter α) : @nhds α (nhdsAdjoint a f) = update pure a (pure a ⊔ f)$$

Lean4

theorem nhds_nhdsAdjoint [DecidableEq α] (a : α) (f : Filter α) :
    @nhds α (nhdsAdjoint a f) = update pure a (pure a ⊔ f) :=
  eq_update_iff.2 ⟨nhds_nhdsAdjoint_same .., fun _ ↦ nhds_nhdsAdjoint_of_ne _⟩

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