instIsUpperWithUpper

Mathlib.Topology.Order.LowerUpperTopology

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

English

If α is a preorder, then WithUpper α inherits the order so that a ≤ b in WithUpper α iff a ≤ b in α.

Русский

Если α имеет предпорядок, то WithUpper α наследует порядок так же, как и α.

LaTeX

$$$\\forall a,b : WithUpper α,\\ a \\le b \\iff a \\le b$$$

Lean4

instance [Preorder α] : IsUpper (WithUpper α) :=
  ⟨rfl⟩

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

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

Разделы

Аффилиация

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