instIsIrreflLex — Mathlib

English

If IsIrrefl ι r and ∀i IsIrrefl (α i) (s i), then Lex r s is irreflexive.

Русский

Если IsIrrefl ι r и ∀i IsIrrefl (α i) (s i), то Lex r s иррефлексивен.

LaTeX

$$$[IsIrrefl ι r]\\ [\\forall i, IsIrrefl (\\alpha i)(s i)] : IsIrrefl ( (i,\\alpha i) ) (Sigma.Lex r s).$$$

Lean4

instance [IsIrrefl ι r] [∀ i, IsIrrefl (α i) (s i)] : IsIrrefl _ (Lex r s) :=
  ⟨by
    rintro _ (⟨a, b, hi⟩ | ⟨a, b, ha⟩)
    · exact irrefl _ hi
    · exact irrefl _ ha⟩

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