nhdsGT_basis — Mathlib

English

In a space with NoMaxOrder, the right neighborhood basis at a is given by intervals Ioo a x with a < x.

Русский

В пространстве без максимума правая окрестность в a задается интервалами Ioo a x, где a < x.

LaTeX

$$$\text{NoMaxOrder}(\alpha) \Rightarrow (\text{nhdsWithin a (Ioi a)} \text{ HasBasis }(\lt a) (Ioo a))$$$

Lean4

theorem nhdsGT_basis [NoMaxOrder α] (a : α) : (𝓝[>] a).HasBasis (a < ·) (Ioo a) :=
  nhdsGT_basis_of_exists_gt <| exists_gt a

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