mem_nhds_top_iff — Mathlib

English

A subset s of EReal is a neighborhood of ⊤ if and only if there exists y ∈ ℝ with Ioi y ⊆ s.

Русский

Подмножество s EReal является окрестностью ⊤ тогда и только тогда, когда существует y ∈ ℝ с Ioi y ⊆ s.

LaTeX

$$$s \\in 𝓝(\\top) \\iff \\exists y\\in\\mathbb{R}, Ioi(y) \\subseteq s$$$

Lean4

theorem mem_nhds_top_iff {s : Set EReal} : s ∈ 𝓝 (⊤ : EReal) ↔ ∃ y : ℝ, Ioi (y : EReal) ⊆ s :=
  nhds_top_basis.mem_iff.trans <| by simp only [true_and]

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