nhds_pure — Mathlib

English

The neighborhood of the pure x is the principal filter on the pair {⊥, pure x}: 𝓝(pure x) = 𝓟({⊥, pure x}).

Русский

Окрестности чистого x равны принципиальному фильтру, порождённому {⊥, pure x}.

LaTeX

$$$\forall x,\; 𝓝(\text{pure } x) = \mathcal{P}\{\bot, \text{pure } x\}.$$$

Lean4

@[simp]
theorem nhds_pure (x : α) : 𝓝 (pure x : Filter α) = 𝓟 {⊥, pure x} := by
  rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]

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