mem_nhdsLE_iff_exists_Ioc_subset'

English

In the NoMinOrder setting, s ∈ nhdsWithin a (Iic a) iff there exists l < a with 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`, provided `a` is not a bottom element. -/
theorem mem_nhdsLE_iff_exists_Ioc_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 4 (by simp) (by simp)

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