Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 10:02 7ddb9a3c

View on Github →

refactor(order/ideal): Generalize definition and lemmas (#11421)

  • Generalize the order_top instance to [nonempty P] [is_directed P (≤)].
  • Delete order.ideal.ideal_inter_nonempty in favor of the equivalent condition is_directed P (swap (≤)).
  • Delete order.ideal.sup/order.ideal.inf in favor of a direct instance declaration.
  • Generalize defs/lemmas from preorder to has_le or partial_order to preorder.
  • Two more is_directed lemmas and instances for order_bot and order_top.

Estimated changes

modified def is_atom
modified def is_coatom
added theorem directed_id_iff
added theorem directed_on_univ
added theorem directed_on_univ_iff
modified theorem is_coatom.is_maximal
modified theorem is_coatom.is_proper
modified theorem order.ideal.bot_mem
added theorem order.ideal.coe_inj
modified theorem order.ideal.coe_top
deleted theorem order.ideal.ext'_iff
modified theorem order.ideal.ext
added theorem order.ideal.ext_iff
deleted theorem order.ideal.ext_set_eq
deleted def order.ideal.inf
modified theorem order.ideal.inter_nonempty
deleted theorem order.ideal.is_ideal
modified theorem order.ideal.mem_inf
modified theorem order.ideal.mem_principal
modified theorem order.ideal.mem_sup
deleted def order.ideal.sup
deleted theorem order.ideal.sup_le
modified structure order.ideal
modified structure order.is_ideal
modified theorem order.mem_ideal_of_cofinals