mem_nhdsLE_iff_exists_Ioc_subset — Mathlib

English

In the NoMinOrder setting, s ∈ nhdsWithin a (Iic a) iff there exists l with l < a and Ioc l a ⊆ s.

Русский

В NoMinOrder: s ∈ nhdsWithin a (Iic a) эквивалентно существованию l < a с Ioc l a ⊆ s.

LaTeX

$$$s \in \mathcal{N}_{[\le]} a \iff \exists l \in Iio(a), Ioc(l,a) \subseteq s$$

Lean4

/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]`
with `l < a`. -/
theorem mem_nhdsLE_iff_exists_Ioc_subset [NoMinOrder α] {a : α} {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  let ⟨_, hl'⟩ := exists_lt a
  mem_nhdsLE_iff_exists_Ioc_subset' hl'

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