Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-29 19:03 45904fba

View on Github →

chore(*): change notation for set.compl (#3212)

  • introduce typeclass has_compl and notation ∁ for has_compl.compl
  • use it instead of has_neg for set and boolean_algebra

Estimated changes

modified theorem set.indicator_compl
modified theorem pfun.compl_dom_subset_core
modified theorem pfun.core_eq
modified theorem pfun.core_res
modified theorem set.compl_compl
modified theorem set.compl_empty
modified theorem set.compl_empty_iff
modified theorem set.compl_eq_univ_diff
modified theorem set.compl_image
modified theorem set.compl_inter
modified theorem set.compl_inter_self
modified theorem set.compl_set_of
modified theorem set.compl_singleton_eq
modified theorem set.compl_subset_comm
modified theorem set.compl_subset_compl
modified theorem set.compl_subset_iff_union
modified theorem set.compl_union
modified theorem set.compl_union_self
modified theorem set.compl_univ
modified theorem set.compl_univ_iff
modified theorem set.diff_compl
modified theorem set.diff_eq
deleted theorem set.fix_set_compl
modified theorem set.image_compl_eq
modified theorem set.image_compl_subset
modified theorem set.inter_compl_self
modified theorem set.inter_subset
modified theorem set.mem_compl
modified theorem set.mem_compl_eq
modified theorem set.mem_compl_iff
modified theorem set.mem_compl_singleton_iff
modified theorem set.nonempty_compl
modified theorem set.not_mem_of_mem_compl
modified theorem set.preimage_compl
modified theorem set.subset_compl_comm
modified theorem set.subset_image_compl
modified theorem set.union_compl_self
modified def set.disjointed
modified theorem set.compl_Ici
modified theorem set.compl_Iic
modified theorem set.compl_Iio
modified theorem set.compl_Ioi
modified theorem set.compl_Inter
modified theorem set.compl_Union
modified theorem set.compl_bInter
modified theorem set.compl_bUnion
modified theorem set.disjoint_compl
deleted theorem set.sub_eq_diff
modified theorem is_measurable.compl
modified theorem is_measurable.compl_iff
modified theorem is_measurable.of_compl
deleted theorem is_measurable.sub
modified theorem measure_theory.mem_ae_iff
modified theorem compl_bot
modified theorem compl_compl'
modified theorem compl_inf
modified theorem compl_inf_eq_bot
modified theorem compl_inj_iff
modified theorem compl_injective
modified theorem compl_le_compl
modified theorem compl_le_compl_iff_le
modified theorem compl_le_iff_compl_le
modified theorem compl_le_of_compl_le
modified theorem compl_sup
modified theorem compl_sup_eq_top
modified theorem compl_top
modified theorem compl_unique
modified theorem inf_compl_eq_bot
added theorem is_compl.compl_eq
deleted theorem is_compl.neg_eq
added theorem is_compl_compl
deleted theorem is_compl_neg
modified theorem le_compl_of_le_compl
added theorem sdiff_eq
added theorem sdiff_eq_left
added theorem sdiff_le_sdiff
deleted theorem sub_eq
deleted theorem sub_eq_left
modified theorem sup_compl_eq_top
added theorem sup_sdiff_same
deleted theorem sup_sub_same
modified theorem compl_Inf
modified theorem compl_Sup
modified theorem compl_infi
modified theorem compl_supr
modified theorem filter.inf_principal_eq_bot
modified theorem filter.is_compl_principal
modified theorem filter.mem_sets_of_eq_bot
modified theorem filter.mem_cofinite
modified theorem cardinal.mk_sum_compl
modified theorem closure_compl
modified theorem closure_diff
modified theorem frontier_compl
modified theorem interior_compl
modified def is_closed
modified theorem is_closed_compl_iff
modified theorem is_open_compl_iff
modified theorem compl_singleton_mem_nhds
modified theorem is_clopen_compl
modified theorem is_clopen_compl_iff
modified theorem is_clopen_diff