Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 04:29 df4066cf

View on Github →

refactor(order/ideal): Make order.ideal extend lower_set (#13070)

  • Redefine order.ideal to extend lower_set.
  • set_like instance
  • Get rid of order.ideal.ideal_Inter_nonempty in favor of order_bot
  • Make arguments to order.ideal.sup_mem semi-implicit
  • Reorder sections according to typeclass assumptions (some were outdated since Yakov's order_bot/order_top refactor)

Estimated changes

deleted theorem order.ideal.Inf_le
modified theorem order.ideal.bot_mem
modified theorem order.ideal.coe_Inf
added theorem order.ideal.coe_inf
deleted theorem order.ideal.coe_inj
deleted theorem order.ideal.coe_injective
added theorem order.ideal.coe_sup
modified theorem order.ideal.coe_top
modified theorem order.ideal.ext
deleted theorem order.ideal.ext_iff
deleted theorem order.ideal.is_glb_Inf
deleted theorem order.ideal.le_Inf
modified theorem order.ideal.mem_Inf
deleted theorem order.ideal.mem_coe
modified theorem order.ideal.mem_compl_of_ge
modified def order.ideal.principal
modified theorem order.ideal.sup_mem
modified theorem order.ideal.top_of_top_mem
modified structure order.ideal
modified theorem order.pfilter.ext
modified theorem order.pfilter.inf_mem
modified theorem order.pfilter.mem_of_le
modified theorem order.pfilter.top_mem