instIsTransLiftRel — Mathlib

English

The transitivity axiom for LiftRel is given by the explicit case analysis on the left or right injections.

Русский

Для LiftRel транзитивность задаётся через явный разбор по случаям на вложения слева и справа.

LaTeX

$$$[IsTrans \\; α\\ r] [IsTrans \\; β\\ s] → ∀ {a b c}, LiftRel r s a b → LiftRel r s b c → LiftRel r s a c$$$

Lean4

instance [IsTrans α r] [IsTrans β s] : IsTrans (α ⊕ β) (LiftRel r s) :=
  ⟨fun _ _ _ => LiftRel.trans _ _⟩

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