nhdsGT_eq_nhdsNE — Mathlib

English

For any a, the right-neighborhood equals the punctured neighborhood: 𝓝[> ] a = 𝓝[≠] a.

Русский

Для любого a правая окрестность равна проколотой окрестности: 𝓝[> ] a = 𝓝[≠] a.

LaTeX

$$$[PredOrder\ α] \; \forall a:\, α,\; 𝓝_{[>]}(a) = 𝓝_{[\neq]}(a)$$$

Lean4

theorem nhdsGT_eq_nhdsNE [PredOrder α] (a : α) : 𝓝[>] a = 𝓝[≠] a := by
  rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

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