instIsTotalLexOfIsTrichotomous — Mathlib

English

If IsTrichotomous ι r and IsTotal (α i) (s i) for all i, then Lex r s is total on the Sigma type.

Русский

Если IsTrichotomous ι r и ∀i IsTotal (α i) (s i), то Lex r s тождественно суммарному Σ-типу.

LaTeX

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

Lean4

instance [IsTrichotomous ι r] [∀ i, IsTotal (α i) (s i)] : IsTotal _ (Lex r s) :=
  ⟨by
    rintro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (Lex.left _ _ hij)
    · obtain hab | hba := total_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Lex.right _ _ hba)
    · exact Or.inr (Lex.left _ _ hji)⟩

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