Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-04 15:22 e4fb6414

View on Github →

feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281) Generalize lemmas from (generalized_)boolean_algebra to (generalized_)coheyting_algebra. Dualize (some of) them. Duplicate lemmas have been made aliases. Add supporting lemmas to golf the proofs.

Estimated changes

modified theorem finset.union_sdiff_symm
modified theorem set.diff_union_self
modified theorem set.subset_compl_comm
modified theorem set.union_diff_self
deleted theorem set.fin.coe_cast_add_zero
modified theorem compl_compl
modified theorem compl_inf
deleted theorem compl_unique
deleted theorem disjoint.sdiff_eq_left
deleted theorem disjoint.sdiff_eq_right
deleted theorem inf_sdiff_left
deleted theorem inf_sdiff_right
deleted theorem inf_sdiff_sup_left
deleted theorem inf_sdiff_sup_right
deleted theorem is_compl.compl_eq
deleted theorem is_compl.eq_compl
deleted theorem le_compl_iff_le_compl
deleted theorem le_compl_of_le_compl
deleted theorem sdiff_idem
deleted theorem sdiff_le'
deleted theorem sdiff_sdiff_comm
deleted theorem sdiff_sdiff_le
deleted theorem sdiff_sdiff_left
deleted theorem sdiff_sdiff_self
deleted theorem sdiff_sup_cancel
deleted theorem sdiff_sup_sdiff_cancel
deleted theorem sdiff_triangle
deleted theorem sup_le_of_le_sdiff_left
deleted theorem sup_le_of_le_sdiff_right
deleted theorem sup_sdiff
deleted theorem sup_sdiff_cancel'
deleted theorem sup_sdiff_cancel_right
deleted theorem sup_sdiff_eq_sup
deleted theorem sup_sdiff_left
deleted theorem sup_sdiff_left_self
deleted theorem sup_sdiff_right
deleted theorem sup_sdiff_right_self
deleted theorem sup_sdiff_self_left
deleted theorem sup_sdiff_self_right
deleted theorem sup_sdiff_symm
modified theorem top_sdiff
added theorem compl_unique
added theorem disjoint.sdiff_eq_left
added theorem himp_inf_himp_cancel
deleted theorem himp_le_himp_himp
added theorem himp_le_himp_himp_himp
added theorem himp_triangle
added theorem inf_sdiff_left
added theorem inf_sdiff_right
added theorem inf_sdiff_sup_left
added theorem inf_sdiff_sup_right
added theorem is_compl.compl_eq
added theorem is_compl.eq_compl
added theorem is_compl.eq_hnot
added theorem is_compl.hnot_eq
modified theorem le_himp_comm
added theorem le_himp_himp
added theorem le_himp_iff'
added theorem sdiff_idem
modified theorem sdiff_le_comm
added theorem sdiff_le_iff'
added theorem sdiff_sdiff_comm
added theorem sdiff_sdiff_le
deleted theorem sdiff_sdiff_le_sdiff
added theorem sdiff_sdiff_left
added theorem sdiff_sdiff_self
added theorem sdiff_sup_cancel
added theorem sdiff_sup_sdiff_cancel
added theorem sdiff_triangle
added theorem sup_sdiff
added theorem sup_sdiff_cancel'
added theorem sup_sdiff_cancel_right
added theorem sup_sdiff_eq_sup
added theorem sup_sdiff_left
added theorem sup_sdiff_left_self
added theorem sup_sdiff_right
added theorem sup_sdiff_right_self
modified theorem inf_eq_left
modified theorem inf_eq_right
deleted theorem inf_of_le_left
deleted theorem inf_of_le_right
deleted theorem le_of_inf_eq
deleted theorem le_of_sup_eq
modified theorem left_eq_inf
modified theorem left_eq_sup
modified theorem right_eq_inf
modified theorem right_eq_sup
modified theorem sup_eq_left
modified theorem sup_eq_right
added theorem sup_le_inf
deleted theorem sup_of_le_left
deleted theorem sup_of_le_right