isPreorder

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelEmbedding.isPreorder

English

If s is a preorder on β, then r is a preorder on α.

Русский

Если s образует предorder на β, то r образует предorder на α.

LaTeX

$$$\text{IsPreorder } \alpha\ r$$$

Lean4

protected theorem isPreorder : ∀ (_ : r ↪r s) [IsPreorder β s], IsPreorder α r
  | f, _ => { f.isRefl, f.isTrans with }

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

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

Разделы

Аффилиация

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