Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-02 09:41 9d57f682

View on Github →

feat(order/bounded_lattice): introduce is_compl predicate (#2569) Also move disjoint from data/set/lattice

Estimated changes

deleted theorem disjoint.comm
deleted theorem disjoint.eq_bot
deleted theorem disjoint.mono
deleted theorem disjoint.mono_left
deleted theorem disjoint.mono_right
deleted theorem disjoint.ne
deleted theorem disjoint.symm
deleted def disjoint
deleted theorem disjoint_bot_left
deleted theorem disjoint_bot_right
deleted theorem disjoint_iff
deleted theorem disjoint_self
added theorem is_compl.neg_eq
added theorem is_compl_neg
added theorem disjoint.comm
added theorem disjoint.eq_bot
added theorem disjoint.mono
added theorem disjoint.mono_left
added theorem disjoint.mono_right
added theorem disjoint.ne
added theorem disjoint.symm
added def disjoint
added theorem disjoint_bot_left
added theorem disjoint_bot_right
added theorem disjoint_iff
added theorem disjoint_self
added theorem is_compl.antimono
added theorem is_compl.inf_eq_bot
added theorem is_compl.inf_sup
added theorem is_compl.le_left_iff
added theorem is_compl.le_right_iff
added theorem is_compl.left_le_iff
added theorem is_compl.left_unique
added theorem is_compl.of_eq
added theorem is_compl.right_le_iff
added theorem is_compl.right_unique
added theorem is_compl.sup_eq_top
added theorem is_compl.sup_inf
added theorem is_compl.to_order_dual
added structure is_compl
added theorem is_compl_bot_top
added theorem is_compl_top_bot
modified theorem filter.map_at_top_eq_of_gc
added theorem eq_of_inf_eq_sup_eq
deleted theorem eq_of_sup_eq_inf_eq
added theorem le_of_inf_le_sup_le