nhds_def — Mathlib

English

The neighborhood filter nhds x is the infimum of principal filters corresponding to open neighborhoods of x.

Русский

Фильтр окрестностей nhds x есть инфимум принципиев над открытыми окрестностями точки x.

LaTeX

$$$nhds(x) = \inf\{ 𝓟(U) : U \text{ открыто}, x \in U \}$$$

Lean4

theorem nhds_def : eta_helper Eq✝ @nhds.{} @(delta% @definition✝) :=
  by
  intros
  delta nhds
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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