isPartialOrder

Mathlib.Order.RelIso.Basic

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

English

If s is a partial order, then r is a partial order on α.

Русский

Если s является частичным порядком, то r является частичным порядком на α.

LaTeX

$$$\text{IsPartialOrder }\alpha\ r$$$

Lean4

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

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

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

Разделы

Аффилиация

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