Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-30 03:44 b449a3cd

View on Github →

feat(order/ideal, order/pfilter, order/prime_ideal): added is_ideal, is_pfilter, is_prime, is_maximal, prime_pair (#6656) Proved basic lemmas about them. Also extended the is_proper API. Made the pfilterarguments of some lemmas explicit:

  • pfilter.nonempty
  • pfilter.directed

Estimated changes

added theorem is_compl.eq_compl
added theorem is_coatom.is_maximal
added theorem is_coatom.is_proper
added theorem order.ideal.ext'_iff
added theorem order.ideal.ext_set_eq
added theorem order.ideal.is_ideal
added theorem order.ideal.top_coe
modified theorem order.ideal.top_of_mem_top
added structure order.is_ideal
added def order.is_pfilter
added theorem order.pfilter.directed
added theorem order.pfilter.ext
added theorem order.pfilter.inf_mem
added theorem order.pfilter.nonempty
added theorem order.pfilter.top_mem
added structure order.pfilter
deleted theorem pfilter.directed
deleted theorem pfilter.ext
deleted theorem pfilter.inf_mem
deleted theorem pfilter.inf_mem_iff
deleted theorem pfilter.mem_of_le
deleted theorem pfilter.mem_of_mem_of_le
deleted theorem pfilter.nonempty
deleted def pfilter.principal
deleted theorem pfilter.principal_le_iff
deleted theorem pfilter.top_mem
deleted structure pfilter
added structure order.ideal.prime_pair