Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 02:18 50a4565f

View on Github →

feat(order/basic): Product of dense orders (#17168) The (arbitrary) product of dense orders is dense.

Estimated changes

added theorem pi.lex.no_max_order'
modified theorem pi.to_lex_monotone
added theorem pi.to_lex_strict_mono
added theorem prod.lex.to_lex_mono
added theorem sigma.lex_swap
added theorem sigma.lex.le_def
added theorem sigma.lex.lt_def
modified theorem le_update_iff
added theorem le_update_self_iff
added theorem lt_update_self_iff
modified theorem update_le_iff
added theorem update_le_self_iff
modified theorem update_le_update_iff
added theorem update_lt_self_iff