instIsLowerSet

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.instIsLowerSet

English

For a preorder α, WithLowerSet α has the lower-set property (IsLowerSet).

Русский

Для предпорядка α пространство WithLowerSet α обладает свойством нижнего множества.

LaTeX

$$$ \forall \alpha [\text{Preorder } \alpha], \operatorname{IsLowerSet} (\mathrm{WithLowerSet}\alpha).$$$

Lean4

instance [Preorder α] : @Topology.IsLowerSet α (lowerSet α) _ :=
  by
  letI := lowerSet α
  exact ⟨rfl⟩

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

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

Разделы

Аффилиация

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