nhdsGT_basis_of_exists_gt — Mathlib

English

If there exists a rightward point above a, then 𝓝[>] a has a basis consisting of sets determined by lt a x and Ioo a x.

Русский

Если существует точка справа от a, тогда окрестность справа имеет базис, задаваемый через lt a x и Ioo a x.

LaTeX

$$$\text{nhdsGT_basis_of_exists_gt} \Rightarrow (\mathcal{nhdsWithin a (Ioi a)}\text{ HasBasis }(\lt a) (Ioo a))$$$

Lean4

theorem nhdsGT_basis_of_exists_gt {a : α} (h : ∃ b, a < b) : (𝓝[>] a).HasBasis (a < ·) (Ioo a) :=
  let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsGT_iff_exists_Ioo_subset' h⟩

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