instIsReflLex — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall {α} {β} {r} {s} [IsRefl α r], IsRefl (Prod α β) (Prod.Lex r s).$$$

Lean4

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

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