isStrictOrder — Mathlib

English

The relation < on DegLex(α →₀ ℕ) is a strict order when α is linearly ordered.

Русский

Отношение < на DegLex(α →₀ ℕ) является строгим порядком, если α линейно упорядочено.

LaTeX

$$$\text{IsStrictOrder}\left(\DegLex(\alpha \to\_0 \mathbb{N}),\; <\right)$$$

Lean4

instance isStrictOrder : IsStrictOrder (DegLex (α →₀ ℕ)) (· < ·)
    where
  irrefl := fun a ↦ by simp [lt_def]
  trans := by
    intro a b c hab hbc
    simp only [lt_iff] at hab hbc ⊢
    rcases hab with (hab | hab)
    · rcases hbc with (hbc | hbc)
      · left; exact lt_trans hab hbc
      · left; exact lt_of_lt_of_eq hab hbc.1
    · rcases hbc with (hbc | hbc)
      · left; exact lt_of_eq_of_lt hab.1 hbc
      · right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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