Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-19 13:44 8df86df8

View on Github →

feat(order/ideal, data/set/lattice): when order ideals are a complete lattice (#9084)

Added the ideal_Inter_nonempty property, which states that the intersection of all ideals in the lattice is nonempty.
Proved that when a preorder has the above property and is a semilattice_sup, its ideals are a complete lattice
Added some lemmas about empty intersections in set/lattice, akin to #9033

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.Inter_eq_empty_iff

added theorem set.bInter_eq_empty_iff

added theorem set.nonempty_Inter

added theorem set.nonempty_bInter

added theorem set.nonempty_sInter

deleted theorem set.sInter_nonempty_iff

Modified src/order/ideal.lean

added theorem order.ideal.Inf_le

added theorem order.ideal.Inter_nonempty

added theorem order.ideal.coe_Inf

added theorem order.ideal.coe_top

added theorem order.ideal.ideal_Inter_nonempty.all_Inter_nonempty

added theorem order.ideal.ideal_Inter_nonempty.all_bInter_nonempty

added theorem order.ideal.ideal_Inter_nonempty.exists_all_mem

added theorem order.ideal.ideal_Inter_nonempty_iff

added theorem order.ideal.ideal_Inter_nonempty_of_exists_all_mem

added theorem order.ideal.inter_nonempty

added theorem order.ideal.is_glb_Inf

added theorem order.ideal.le_Inf

added theorem order.ideal.mem_Inf

deleted theorem order.ideal.top_carrier

deleted theorem order.ideal.top_coe

deleted theorem order.inter_nonempty