nhdsGE_basis_Ico — Mathlib

English

Equivalence of several right-neighborhood statements around a and values Ioi, Ico, Ioc, Icc in the ge-side.

Русский

Эквивалентность нескольких утверждений о правой окрестности вокруг a с использованием Ioi, Ico, Ioc, Icc.

LaTeX

$$$\mathrm{TFAE}\!\left[ s \in \mathcal{N}_{[\ge]}(a), s \in \mathcal{N}_{[a,b]}(a), s \in \mathcal{N}_{[a,b)}(a), \exists l \in Ioc(a,b), Ico(a,l) \subseteq s, \exists l \in Ioi(a), Ico(a,l) \subseteq s]$$$

Lean4

theorem nhdsGE_basis_Ico [NoMaxOrder α] (a : α) : (𝓝[≥] a).HasBasis (fun u => a < u) (Ico a) :=
  ⟨fun _ => mem_nhdsGE_iff_exists_Ico_subset⟩

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