Commit 2022-12-06 00:44 c1e117a8

View on Github →

feat: port Order.SymmDiff (#842) mathlib3 SHA: 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904

Estimated changes

added theorem Bool.symmDiff_eq_xor
added theorem IsCompl.bihimp_eq_bot
added theorem Pi.bihimp_apply
added theorem Pi.bihimp_def
added theorem Pi.symmDiff_apply
added theorem Pi.symmDiff_def
added def bihimp
added theorem bihimp_assoc
added theorem bihimp_bihimp_self
added theorem bihimp_bihimp_sup
added theorem bihimp_bot
added theorem bihimp_comm
added theorem bihimp_def
added theorem bihimp_eq'
added theorem bihimp_eq
added theorem bihimp_eq_bot
added theorem bihimp_eq_inf
added theorem bihimp_eq_inf_himp_inf
added theorem bihimp_eq_left
added theorem bihimp_eq_right
added theorem bihimp_eq_top
added theorem bihimp_fst
added theorem bihimp_himp_eq_inf
added theorem bihimp_himp_left
added theorem bihimp_himp_right
added theorem bihimp_hnot_self
added theorem bihimp_iff_iff
added theorem bihimp_inf_sup
added theorem bihimp_le_iff_left
added theorem bihimp_le_iff_right
added theorem bihimp_left_comm
added theorem bihimp_left_inj
added theorem bihimp_left_injective
added theorem bihimp_left_involutive
added theorem bihimp_left_surjective
added theorem bihimp_of_ge
added theorem bihimp_of_le
added theorem bihimp_right_comm
added theorem bihimp_right_inj
added theorem bihimp_right_injective
added theorem bihimp_self
added theorem bihimp_snd
added theorem bihimp_top
added theorem bihimp_triangle
added theorem bot_bihimp
added theorem bot_symmDiff
added theorem codisjoint_bihimp_sup
added theorem compl_bihimp
added theorem compl_bihimp_compl
added theorem compl_bihimp_self
added theorem compl_symmDiff
added theorem compl_symmDiff_compl
added theorem compl_symmDiff_self
added theorem disjoint_symmDiff_inf
added theorem himp_bihimp
added theorem himp_bihimp_eq_inf
added theorem himp_bihimp_left
added theorem himp_bihimp_right
added theorem hnot_symmDiff_self
added theorem inf_himp_bihimp
added theorem inf_le_bihimp
added theorem inf_sup_symmDiff
added theorem inf_symmDiff_symmDiff
added theorem le_bihimp
added theorem le_bihimp_iff
added theorem le_symmDiff_iff_left
added theorem le_symmDiff_iff_right
added theorem ofDual_bihimp
added theorem ofDual_symmDiff
added theorem sdiff_symmDiff'
added theorem sdiff_symmDiff
added theorem sdiff_symmDiff_eq_sup
added theorem sdiff_symmDiff_left
added theorem sdiff_symmDiff_right
added theorem sup_bihimp_bihimp
added theorem sup_himp_bihimp
added theorem sup_inf_bihimp
added theorem sup_sdiff_symmDiff
added def symmDiff
added theorem symmDiff_assoc
added theorem symmDiff_bot
added theorem symmDiff_comm
added theorem symmDiff_compl_self
added theorem symmDiff_def
added theorem symmDiff_eq'
added theorem symmDiff_eq
added theorem symmDiff_eq_Xor'
added theorem symmDiff_eq_bot
added theorem symmDiff_eq_left
added theorem symmDiff_eq_right
added theorem symmDiff_eq_sup
added theorem symmDiff_eq_top
added theorem symmDiff_fst
added theorem symmDiff_hnot_self
added theorem symmDiff_le
added theorem symmDiff_le_iff
added theorem symmDiff_le_sup
added theorem symmDiff_left_comm
added theorem symmDiff_left_inj
added theorem symmDiff_of_ge
added theorem symmDiff_of_le
added theorem symmDiff_right_comm
added theorem symmDiff_right_inj
added theorem symmDiff_sdiff
added theorem symmDiff_sdiff_eq_sup
added theorem symmDiff_sdiff_inf
added theorem symmDiff_sdiff_left
added theorem symmDiff_sdiff_right
added theorem symmDiff_self
added theorem symmDiff_snd
added theorem symmDiff_sup_inf
added theorem symmDiff_symmDiff_inf
added theorem symmDiff_symmDiff_left
added theorem symmDiff_top'
added theorem symmDiff_top
added theorem symmDiff_triangle
added theorem toDual_bihimp
added theorem toDual_symmDiff
added theorem top_bihimp
added theorem top_symmDiff'
added theorem top_symmDiff