limsSup_nhds — Mathlib

English

In a conditionally complete linear order with order topology, limsSup of nhds a is a.

Русский

В условно завершимом линейном порядке сorder topology, limsSup nhds(a) равен a.

LaTeX

$$$ limsSup (\mathcal{N}a) = a. $$$

Lean4

theorem limsSup_nhds (a : α) : limsSup (𝓝 a) = a :=
  csInf_eq_of_forall_ge_of_forall_gt_exists_lt (isBounded_le_nhds a)
    (fun a' (h : {n : α | n ≤ a'} ∈ 𝓝 a) ↦ show a ≤ a' from @mem_of_mem_nhds _ _ a _ h) fun b (hba : a < b) ↦
    show ∃ c, {n : α | n ≤ c} ∈ 𝓝 a ∧ c < b from
      match dense_or_discrete a b with
      | Or.inl ⟨c, hac, hcb⟩ => ⟨c, ge_mem_nhds hac, hcb⟩
      | Or.inr ⟨_, h⟩ => ⟨a, (𝓝 a).sets_of_superset (gt_mem_nhds hba) h, hba⟩

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