nhdsLT_basis_of_exists_lt — Mathlib

English

If there exists some b < a, then the left-neighborhood filter of a has a basis given by sets Ioo(x,a) with x < a.

Русский

Если существует b < a, то норма слева имеет базис из множеств Ioo(x,a) при x < a.

LaTeX

$$$(\exists b, b < a) \Rightarrow (\mathcal{N}_{(-\infty,a)}(a)) \text{ has basis } (x < a)\mapsto Ioo(x,a)$$

Lean4

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

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