Commit 2022-12-02 17:14 608fd2f6

View on Github →

feat: port Order.BooleanAlgebra (#794) mathlib3 sha 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

added theorem Bool.compl_eq_bnot
added theorem Bool.inf_eq_band
added theorem Bool.sup_eq_bor
added theorem IsCompl.compl_eq_iff
added theorem compl_bijective
added theorem compl_comp_compl
added theorem compl_compl
added theorem compl_eq_bot
added theorem compl_eq_comm
added theorem compl_eq_iff_is_compl
added theorem compl_eq_top
added theorem compl_himp
added theorem compl_himp_compl
added theorem compl_inf
added theorem compl_inj_iff
added theorem compl_injective
added theorem compl_involutive
added theorem compl_le_compl_iff_le
added theorem compl_le_iff_compl_le
added theorem compl_le_of_compl_le
added theorem compl_sdiff
added theorem compl_sdiff_compl
added theorem compl_sup_eq_top
added theorem compl_surjective
added theorem disjoint_inf_sdiff
added theorem disjoint_sdiff_iff_le
added theorem disjoint_sdiff_sdiff
added theorem eq_compl_comm
added theorem eq_compl_iff_is_compl
added theorem eq_of_sdiff_eq_sdiff
added theorem himp_eq
added theorem hnot_eq_compl
added theorem inf_compl_eq_bot'
added theorem inf_inf_sdiff
added theorem inf_sdiff
added theorem inf_sdiff_assoc
added theorem inf_sdiff_distrib_left
added theorem inf_sdiff_eq_bot_iff
added theorem inf_sdiff_inf
added theorem inf_sdiff_right_comm
added theorem inf_sdiff_self_left
added theorem inf_sdiff_self_right
added theorem is_compl_compl
added theorem le_iff_disjoint_sdiff
added theorem le_iff_eq_sup_sdiff
added theorem le_sdiff_iff
added theorem sdiff_compl
added theorem sdiff_eq
added theorem sdiff_eq_comm
added theorem sdiff_eq_symm
added theorem sdiff_inf_sdiff
added theorem sdiff_lt
added theorem sdiff_lt_sdiff_right
added theorem sdiff_sdiff_eq_self
added theorem sdiff_sdiff_left'
added theorem sdiff_sdiff_right'
added theorem sdiff_sdiff_right
added theorem sdiff_sdiff_right_self
added theorem sdiff_sdiff_sup_sdiff'
added theorem sdiff_sdiff_sup_sdiff
added theorem sdiff_sup
added theorem sdiff_unique
added theorem sup_compl_eq_top
added theorem sup_inf_inf_compl
added theorem sup_inf_inf_sdiff
added theorem sup_inf_sdiff
added theorem sup_sdiff_inf
added theorem top_sdiff