Icc_mem_nhds_iff — Mathlib

English

Icc a b ∈ nhds x if and only if x ∈ Ioo a b, given no endpoints.

Русский

Icc a b принадлежит nhds x тогда и только тогда, когда x ∈ Ioo(a,b), при отсутствии крайних точек.

LaTeX

$$$ Icc(a,b) \in \nhds(x) \iff x \in Ioo(a,b) $$$

Lean4

@[simp]
theorem Icc_mem_nhds_iff [NoMinOrder α] [NoMaxOrder α] {a b x : α} : Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
  rw [← interior_Icc, mem_interior_iff_mem_nhds]

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