preorder — Mathlib

English

The lexicographical linear order on the dependent sigma type Σₗ' i, α i is a preorder; that is, it satisfies reflexivity and transitivity, together with lt-iff-le-not_ge equivalence.

Русский

Лексикографический линейный порядок над зависимой сигма-типом Σₗ' i, α i образует предократноe множество: рефлексивность, транзитивность и эквивалентность между lt и le/not ge.

LaTeX

$$$\\text{Preorder}(\\Sigma'_i \\alpha_i, \\le_{\\mathrm{Lex}})$$$

Lean4

instance preorder [Preorder ι] [∀ i, Preorder (α i)] : Preorder (Σₗ' i, α i) :=
  { Lex.le, Lex.lt with le_refl := fun ⟨_, _⟩ => Lex.right _ le_rfl,
    le_trans := by
      rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ ⟨h₁r⟩ ⟨h₂r⟩
      · left
        apply lt_trans
        repeat' assumption
      · left
        assumption
      · left
        assumption
      · right
        apply le_trans
        repeat' assumption,
    lt_iff_le_not_ge :=
      by
      refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨i, a, hji⟩ | ⟨i, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba
      · rintro ⟨⟨j, b, hij⟩ | ⟨i, hab⟩, hba⟩
        · exact Lex.left _ _ hij
        · exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h) }

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