isTrichotomous_lex — Mathlib

English

If each coordinate relation s is trichotomous and r is well-founded, then the Lex product relation is trichotomous.

Русский

Если каждая координата имеет отношение тричотомии и r хорошо упорядочено, то отношения Lex тричотомичны.

LaTeX

$$$ IsTrichotomous(\\text{Lex}((i\\mapsto \\beta_i)), <) $ under given hypotheses$$

Lean4

theorem isTrichotomous_lex [∀ i, IsTrichotomous (β i) s] (wf : WellFounded r) :
    IsTrichotomous (∀ i, β i) (Pi.Lex r @s) :=
  {
    trichotomous := fun a b => by
      rcases eq_or_ne a b with hab | hab
      · exact Or.inr (Or.inl hab)
      · rw [Function.ne_iff] at hab
        let i := wf.min _ hab
        have hri : ∀ j, r j i → a j = b j := by
          intro j
          rw [← not_imp_not]
          exact fun h' => wf.not_lt_min _ _ h'
        have hne : a i ≠ b i := wf.min_mem _ hab
        rcases trichotomous_of s (a i) (b i) with hi | hi
        exacts [Or.inl ⟨i, hri, hi⟩, Or.inr <| Or.inr <| ⟨i, fun j hj => (hri j hj).symm, hi.resolve_left hne⟩] }

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