mem_nhds_bot_iff — Mathlib

English

A subset s of EReal is in 𝓝(⊥) if and only if there exists y ∈ ℝ with Iio (y) ⊆ s.

Русский

Множество s принадлежит 𝓝(⊥) тогда и только тогда, когда существует y ∈ ℝ, такое что Iio(y) ⊆ s.

LaTeX

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

Lean4

theorem mem_nhds_bot_iff {s : Set EReal} : s ∈ 𝓝 (⊥ : EReal) ↔ ∃ y : ℝ, Iio (y : EReal) ⊆ s :=
  nhds_bot_basis.mem_iff.trans <| by simp only [true_and]

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