mem_nhdsLT_iff_exists_Ioo_subset — Mathlib

English

If NoMinOrder and densely ordered, then s ∈ nhdsLeft(a) iff there exists l' < a with Ioo(l',a) ⊆ s.

Русский

Если есть минимальный элемент и плотно упорядочено, то s является левой окрестностью a тогда и только тогда существует l' < a, такое что (l', a) ⊆ s.

LaTeX

$$$s \in \mathcal{N}_{(-\infty,a)}(a) \iff \exists l'\!<\!a\, (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_Ioo_subset [NoMinOrder α] {a : α} {s : Set α} : s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s :=
  let ⟨_, h⟩ := exists_lt a
  mem_nhdsLT_iff_exists_Ioo_subset' h

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