nhdsGE_eq_iInf_inf_principal — Mathlib

English

Under suitable hypotheses, the induced topology by f coincides with the preorder topology on α.

Русский

При подходящих условиях индуцированная топология через f совпадает с ордерной топологией на α.

LaTeX

$$$\\mathrm{induced}(f) = \\mathrm{Preorder.topology}(α).$$$

Lean4

theorem nhdsGE_eq_iInf_inf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] (a : α) :
    𝓝[≥] a = (⨅ (u) (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) :=
  by
  rw [nhdsWithin, nhds_eq_order]
  refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)
  exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)

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