instIsReflLiftRel — Mathlib

English

The instance introduces that LiftRel r s is reflexive on α ⊕ β when r and s are reflexive on α and β respectively.

Русский

Пример показывает, что LiftRel r s рефлексивно на α ⊕ β, если r и s рефлексивны на α и β.

LaTeX

$$$[IsRefl\\; α\\ r] \\Rightarrow [IsRefl\\; β\\ s] \\Rightarrow IsRefl(\\alpha \\oplus \\beta)(LiftRel r s)$$$

Lean4

instance [IsRefl α r] [IsRefl β s] : IsRefl (α ⊕ β) (LiftRel r s) :=
  ⟨LiftRel.refl _ _⟩

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