instIsReflLex — Mathlib

English

If r and s are reflexive, then the Lex relation is reflexive on Sum α β, i.e., every element is related to itself in Lex.

Русский

Если r и s рефлексивны, то в Sum α β отношение Lex рефлексивно: каждый элемент связан с самим собой.

LaTeX

$$$[IsRefl \\; α \\ r] [IsRefl \\; β \\ s] ⇒ IsRefl(\\mathrm{Sum}(α,β))(\\mathrm{Lex}(r,s))$$$

Lean4

instance [IsRefl α r] [IsRefl β s] : IsRefl (α ⊕ β) (Lex r s) :=
  ⟨by
    rintro (a | a)
    exacts [Lex.inl (refl _), Lex.inr (refl _)]⟩

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