nhdsLT_eq_nhdsNE — Mathlib

English

In a succ-order, the left-neighborhood equals the right-neighborhood of the complement; i.e., 𝓝[<] a = 𝓝[≠] a.

Русский

Вsucc-порядке левая окрестность равна правой окрестности дополнения; то есть 𝓝[<] a = 𝓝[≠] a.

LaTeX

$$$\mathsf{nhds}_{[<]} a = \mathsf{nhds}_{[\neq]} a$$$

Lean4

theorem nhdsLT_eq_nhdsNE [SuccOrder α] (a : α) : 𝓝[<] a = 𝓝[≠] a :=
  PredOrder.nhdsGT_eq_nhdsNE (α := αᵒᵈ) a

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