isStrictOrder — Mathlib

English

If ι is linearly ordered and each coordinate has a partial order, then the Lex order on DFinsupps is a strict order.

Русский

Если ι упорядочен линейно и в каждой координате задан частичный порядок, то Lex-порядок на DFinsupp является строгим порядком.

LaTeX

$$instance isStrictOrder [∀ i, PartialOrder (α i)] : IsStrictOrder (Lex (Π₀ i, α i)) (· < ·)$$

Lean4

instance isStrictOrder [∀ i, PartialOrder (α i)] : IsStrictOrder (Lex (Π₀ i, α i)) (· < ·)
    where
  irrefl _ := lt_irrefl (α := Lex (∀ i, α i)) _
  trans _ _ _ := lt_trans (α := Lex (∀ i, α i))

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