disjoint_nhds_atTop_iff — Mathlib

English

The neighborhoods of a point a and the ray atTop are disjoint if and only if a is not a top element.

Русский

Окрестности точки a и луча atTop не пересекаются тогда и только тогда, когда a не является верхним элементом.

LaTeX

$$$ Disjoint(\mathcal{N} a, atTop) \iff \neg IsTop(a) $$$

Lean4

@[simp]
theorem disjoint_nhds_atTop_iff : Disjoint (𝓝 a) atTop ↔ ¬IsTop a :=
  disjoint_nhds_atBot_iff (α := αᵒᵈ)

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