instIsIrreflLex — Mathlib

English

If r on α and s on β are irreflexive, then the lexicographic order on α ⊕ β, built from r and s, is irreflexive as well. In other words, no element of α ⊕ β is related to itself under the Lex order built from r and s.

Русский

Если r на α и s на β иррефлексивны, то лексикографический порядок на α ⊕ β, построенный из r и s, тоже иррефлексивен. Другими словами, ни один элемент α ⊕ β не связан с самим собой относительно порядка Lex.

LaTeX

$$$\operatorname{IsIrrefl}(\alpha \oplus \beta, \mathrm{Lex}(r,s))$$$

Lean4

instance [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α ⊕ β) (Lex r s) :=
  ⟨by rintro _ (⟨h⟩ | ⟨h⟩) <;> exact irrefl _ h⟩

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