mem_nhdsGE_iff_exists_Icc_subset — Mathlib

English

A left-neighborhood within (-∞, a] contains some interval [l, a] with l < a.

Русский

Левая окрестность в (-∞, a] содержит интервал [l, a] с l < a.

LaTeX

$$$s \in \mathcal{N}_{[\le]} a \iff \exists l, l < a \land 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`. -/
theorem mem_nhdsGE_iff_exists_Icc_subset [NoMaxOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[≥] a ↔ ∃ u, a < u ∧ Icc a u ⊆ s :=
  nhdsGE_basis_Icc.mem_iff

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