nhdsLT — Mathlib

English

In a PredOrder, the left-neighborhood of any a is the bottom filter: 𝓝[<] a = ⊥.

Русский

В предпорядке левая окрестность точки равна нулевому фильтру: 𝓝[<] a = ⊥.

LaTeX

$$$[PredOrder\ α] \; \forall a:\, α,\; \mathcal{N}_{[<]}(a) = \bot$$$

Lean4

protected theorem nhdsLT [PredOrder α] : 𝓝[<] a = ⊥ := by
  if h : IsMin a then simp [h.Iio_eq] else exact (Order.pred_covBy_of_not_isMin h).nhdsLT

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