Commit 2025-10-02 15:37 3a826f51

View on Github →

feat: Colex order on pi types (#29080) We define an order instance on Colex (∀ i, β i), so that its < relation is Pi.Lex (· > ·) (· < ·).

Estimated changes

Modified Mathlib/Order/PiLex.lean

added theorem Pi.Colex.noMaxOrder'

added theorem Pi.colex_asc

added theorem Pi.le_toColex_update_self_iff

added theorem Pi.lt_toColex_update_self_iff

added theorem Pi.toColex_monotone

added theorem Pi.toColex_strictMono

added theorem Pi.toColex_update_le_self_iff

added theorem Pi.toColex_update_lt_self_iff