nhdsLT_basis

Mathlib.Topology.Order.LeftRightNhds

URI: https://scilib.ai/kg/mathlib#nhdsLT_basis

English

For NoMinOrder α, the left-neighborhood filter of any a has a basis given by Ioo intervals to a.

Русский

Для NoMinOrder α: базис левых окрестностей состоит из интервалов Ioo(x,a).

LaTeX

$$$\forall a, (\mathcal{N}_{(-\infty,a)}(a)).HasBasis (\lambda x. x < a) (Ioo(,a))$$

Lean4

theorem nhdsLT_basis [NoMinOrder α] (a : α) : (𝓝[<] a).HasBasis (· < a) (Ioo · a) :=
  nhdsLT_basis_of_exists_lt <| exists_lt a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru