isIrrefl — Mathlib

English

If α has an irreflexive relation r and β has an irreflexive relation s, then the lexicographic order Prod.Lex r s on α×β is irreflexive.

Русский

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

LaTeX

$$[IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α × β) (Prod.Lex r s)$$

Lean4

instance isIrrefl [IsIrrefl α r] [IsIrrefl β s] : IsIrrefl (α × β) (Prod.Lex r s) :=
  ⟨by rintro ⟨i, a⟩ (⟨_, _, h⟩ | ⟨_, h⟩) <;> exact irrefl _ h⟩

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