refl_right — Mathlib

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 _)

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