mem_nhdsLT_iff_exists_Ico_subset — Mathlib

English

Under NoMinOrder, for any a, s ∈ left-neighborhood of a iff there exists l' < a with Ioo(l', a) ⊆ s.

Русский

При условии NoMinOrder: s ∈ левомуNeighborhood(a) эквивалентно ∃ l' < a: Ioo(l',a) ⊆ s.

LaTeX

$$$s \in \mathcal{N}_{(-\infty,a)}(a) \iff \exists l'\!<\!a, \ Ioo(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_nhdsLT_iff_exists_Ico_subset [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s :=
  by
  have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset
  simpa using this

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