mem_nhdsGE_iff_exists_Ico_subset'

English

In a densely ordered space with no minimum, left-neighborhood around a is characterized by intervals Icc(l,a) with l<a.

Русский

Для плотно упорядоченного пространства без минимума левая окрестность описывается интервалами Icc(l,a) с l<a.

LaTeX

$$$s \in \mathcal{N}_{(-\infty,a)}(a) \iff \exists l \ (< a), Icc(l,a) \subseteq s$$

Lean4

/-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)`
with `a < u < u'`, provided `a` is not a top element. -/
theorem mem_nhdsGE_iff_exists_Ico_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 4 (by simp) (by simp)

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