isOpen_iff_eventually — Mathlib

English

A set s is open iff for every x ∈ s, for all y eventually near x, y ∈ s.

Русский

Множество s открыто тогда и только тогда, когда для каждой x ∈ s и для всех y близких к x вплоть до бесконечности, y ∈ s.

LaTeX

$$$\\text{IsOpen}(s) \\iff \\forall x, x \\in s \\to \\forall^\\mathrm{f} y \\in \\mathcal{N}(x), y \\in s$$$

Lean4

/-- A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`. -/
theorem isOpen_iff_eventually : IsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s :=
  isOpen_iff_mem_nhds

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