instIsIrreflLiftRel

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.instIsIrreflLiftRel

English

If r and s are irreﬂexive on α and β, then LiftRel r s is irreﬂexive on α ⊕ₗ β.

Русский

Если r и s иррефлексивны на α и β, то LiftRel r s иррефлексивен на α ⊕ₗ β.

LaTeX

$$$[IsIrrefl\\; α\\ r] [IsIrrefl\\; β\\ s] ⇒ IsIrrefl(α \\oplus β)(LiftRel r s)$$$

Lean4

instance [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α ⊕ β) (LiftRel r s) :=
  ⟨by rintro _ (⟨h⟩ | ⟨h⟩) <;> exact irrefl _ h⟩

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

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

Разделы

Аффилиация

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