mem_nhdsLE_iff_exists_Icc_subset — Mathlib

English

In a densely ordered NoMinOrder space, left-neighborhood equals existence of l with l<a and Icc(l,a) ⊆ s.

Русский

При плотном порядке и отсутствии минимума: левая окрестность эквивалентна существованию l<a и Icc(l,a) ⊆ s.

LaTeX

$$$s \in \mathcal{N}_{[\le]} a \iff \exists l < a, Icc(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_Icc_subset [NoMinOrder α] [DenselyOrdered α] {a : α} {s : Set α} :
    s ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s :=
  calc
    s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl
    _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' s := mem_nhdsGE_iff_exists_Icc_subset
    _ ↔ ∃ l, l < a ∧ Icc l a ⊆ s := by simp

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