Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 19:44 d136cd55

View on Github →

chore(data/pi/lex): turn pi.lex.linear_order into an instance (#14389)

  • Use [is_well_order ι (<)] instead of (wf : well_founded ((<) : ι → ι → Prop)). This way pi.lex.linear_order can be an instance.
  • Add pi.lex.order_bot/pi.lex.order_top/pi.lex.bounded_order.

Estimated changes

added theorem pi.is_trichotomous_lex
modified theorem pi.lex.le_of_forall_le
added theorem pi.lex.le_of_of_lex_le
added theorem pi.to_lex_monotone