instIsReflLex_1 — Mathlib

English

If s is reflexive on β, then the lexicographic order Prod.Lex r s is reflexive on α×β.

Русский

Если s рефлексивно на β, то лексикографический порядок Prod.Lex r s на α×β рефлексивен.

LaTeX

$$[IsRefl \\beta s] \\Rightarrow IsRefl (α \\times β) (Prod.Lex r s)$$

Lean4

instance {r : α → α → Prop} {s : β → β → Prop} [IsRefl β s] : IsRefl (α × β) (Prod.Lex r s) :=
  ⟨Lex.refl_right _ _⟩

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