nhdsLT_eq_bot_iff — Mathlib

English

The left-neighborhood filter at a is the bottom element iff a is bottom or there exists a predecessor b with b ≺ a.

Русский

Левое окрестностей фильтр в a равен ⊥ тогда, когда a — нульсоответствующий минимум или существует предшественник b с b < a.

LaTeX

$$$\mathcal{N}_{(-\infty,a)}(a) = \bot \iff \text{IsBot}(a) \lor ∃ b, b \prec a$$

Lean4

theorem nhdsLT_eq_bot_iff {a : α} : 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a :=
  by
  convert (config := { preTransparency := .default }) nhdsGT_eq_bot_iff (a := OrderDual.toDual a) using 4
  exact ofDual_covBy_ofDual_iff

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