English
Let r be a relation on α and s a relation on β. If s is reflexive, then the lexicographic order on α×β is reflexive: for every x in α×β, x is related to itself under Prod.Lex r s.
Русский
Пусть r — отношение на α, s — отношение на β. Если s рефлексивно, то лексикографическое отношение на α×β рефлексивно: для каждого x в α×β выполняется x ≤lex x.
LaTeX
$$$[IsRefl\\, \\beta\\, s] \\Rightarrow \\forall x:\\alpha \\times \\beta,\\ Prod.Lex r s\\, x\\, x$$$
Lean4
@[refl]
theorem refl_right (r : α → α → Prop) (s : β → β → Prop) [IsRefl β s] : ∀ x, Prod.Lex r s x x
| (_, _) => Lex.right _ (refl _)