const_lt

Mathlib.Order.Filter.FilterProduct

URI: https://scilib.ai/kg/mathlib#Filter.Germ.const_lt

English

If x < y in β, then the constant germs satisfy (const x) < (const y) in β*.

Русский

Если x < y в β, то константные Гермы удовлетворяют (const x) < (const y) в β*.

LaTeX

$$$x < y \\Rightarrow \\mathrm{Germ}(x) < \\mathrm{Germ}(y).$$$

Lean4

theorem const_lt [Preorder β] {x y : β} : x < y → (↑x : β*) < ↑y :=
  coe_lt.mpr ∘ liftRel_const

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

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

Разделы

Аффилиация

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