Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-07 14:25 c4f3869b

View on Github →

chore(order/symm_diff): Change the symmetric difference notation (#13217) The notation for symm_diff was Δ (\D, \GD, \Delta). It now is ∆ (\increment).

Estimated changes

modified theorem lattice.compl_biimp
modified theorem lattice.compl_symm_diff
modified theorem bot_symm_diff
modified theorem compl_symm_diff
modified theorem compl_symm_diff_self
modified theorem disjoint.symm_diff_eq_sup
modified theorem disjoint_symm_diff_inf
modified theorem inf_symm_diff_distrib_left
modified theorem inf_symm_diff_distrib_right
modified theorem inf_symm_diff_symm_diff
modified theorem is_compl.symm_diff_eq_top
modified theorem sdiff_symm_diff'
modified theorem sdiff_symm_diff
modified theorem sdiff_symm_diff_self
modified theorem sup_sdiff_symm_diff
modified theorem symm_diff_assoc
modified theorem symm_diff_bot
modified theorem symm_diff_comm
modified theorem symm_diff_compl_self
modified theorem symm_diff_eq
modified theorem symm_diff_eq_bot
modified theorem symm_diff_eq_left
modified theorem symm_diff_eq_right
modified theorem symm_diff_eq_sup
modified theorem symm_diff_eq_sup_sdiff_inf
modified theorem symm_diff_eq_top_iff
modified theorem symm_diff_eq_xor
modified theorem symm_diff_le_sup
modified theorem symm_diff_left_inj
modified theorem symm_diff_right_inj
modified theorem symm_diff_sdiff
modified theorem symm_diff_sdiff_left
modified theorem symm_diff_sdiff_right
modified theorem symm_diff_self
modified theorem symm_diff_symm_diff_inf
modified theorem symm_diff_symm_diff_self'
modified theorem symm_diff_symm_diff_self
modified theorem symm_diff_top
modified theorem top_symm_diff