isStrictOrder — Mathlib

English

Under dualization of the index order, Lex inherits a strict order on the Colex type.

Русский

При двойственной перестановке индекса Lex наследует строгий порядок на Colex.

LaTeX

$$IsStrictOrder(Colex(∀ i, β i)) <=> Lex.isStrictOrder under reversed index$$

Lean4

instance isStrictOrder [LinearOrder ι] [∀ a, PartialOrder (β a)] : IsStrictOrder (Colex (∀ i, β i)) (· < ·) :=
  Lex.isStrictOrder (ι := ιᵒᵈ)

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