Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-16 20:46 bdc90f6c

View on Github →

feat(data/set/basic): more set theorems, normalize naming

Estimated changes

Modified algebra/module.lean

deleted theorem set.sInter_eq_Inter

Modified analysis/topology/topological_space.lean

modified theorem is_open_diff

Modified analysis/topology/uniform_space.lean

Modified data/analysis/topology.lean

Modified data/set/basic.lean

added theorem set.compl_subset_compl

added theorem set.diff_eq_empty

added theorem set.diff_eq_self

added theorem set.diff_inter_self

deleted theorem set.diff_neq_empty

deleted theorem set.diff_right_antimono

added theorem set.diff_singleton_eq_self

added theorem set.diff_subset_diff_left

added theorem set.diff_subset_diff_right

added theorem set.diff_union_self

added theorem set.insert_diff

added theorem set.insert_diff_singleton

deleted theorem set.insert_sdiff

added theorem set.inter_diff_assoc

added theorem set.inter_diff_self

modified theorem set.inter_subset_inter_left

modified theorem set.inter_subset_inter_right

added theorem set.inter_union_diff

added theorem set.union_diff_cancel_left

added theorem set.union_diff_cancel_right

added theorem set.union_diff_left

added theorem set.union_diff_right

added theorem set.union_diff_self

added theorem set.union_inter_cancel_left

added theorem set.union_inter_cancel_right

modified theorem set.union_subset_union

added theorem set.union_subset_union_left

added theorem set.union_subset_union_right

Modified data/set/disjointed.lean

Modified data/set/finite.lean

Modified data/set/lattice.lean

added theorem disjoint.comm

added theorem disjoint.eq_bot

added theorem disjoint.symm

modified def disjoint

modified theorem disjoint_bot_left

modified theorem disjoint_bot_right

deleted theorem disjoint_comm

added theorem disjoint_iff

deleted theorem disjoint_symm

added theorem set.Inter_const

modified theorem set.Inter_eq_comp_Union_comp

deleted theorem set.Inter_eq_sInter_image

added theorem set.Inter_eq_sInter_range

added theorem set.Inter_inter_distrib

added theorem set.Inter_subset

added theorem set.Union_const

modified theorem set.Union_eq_comp_Inter_comp

added theorem set.Union_eq_range_sigma

deleted theorem set.Union_eq_sUnion_image

added theorem set.Union_eq_sUnion_range

added theorem set.Union_union_distrib

added theorem set.bInter_eq_Inter

added theorem set.bUnion_eq_Union

modified theorem set.compl_Inter

modified theorem set.compl_Union

deleted theorem set.compl_subset_compl_iff_subset

added theorem set.diff_Inter_left

added theorem set.diff_Union_left

added theorem set.diff_Union_right

added theorem set.disjoint_diff

deleted theorem set.insert_sdiff_singleton

added theorem set.inter_Inter_left

added theorem set.inter_Inter_right

added theorem set.inter_Union_left

added theorem set.inter_Union_right

deleted theorem set.inter_distrib_Union_left

deleted theorem set.inter_distrib_Union_right

added theorem set.inter_eq_Inter

modified theorem set.mem_Inter

deleted theorem set.mem_Inter_eq

added theorem set.mem_Inter_of_mem

added theorem set.mem_Union

deleted theorem set.mem_Union_eq

modified theorem set.mem_sInter

deleted theorem set.mem_sInter_eq

modified theorem set.mem_sUnion

deleted theorem set.mem_sUnion_eq

added theorem set.mem_sUnion_of_mem

added theorem set.range_sigma_eq_Union_range

added theorem set.sInter_eq_Inter

added theorem set.sInter_eq_bInter

modified theorem set.sInter_subset_of_mem

added theorem set.sInter_subset_sInter

deleted theorem set.sUnion_eq_Union'

modified theorem set.sUnion_eq_Union

added theorem set.sUnion_eq_bUnion

modified theorem set.sUnion_subset_iff

added theorem set.sUnion_subset_sUnion

deleted theorem set.sdiff_empty

deleted theorem set.sdiff_eq:

deleted theorem set.sdiff_inter_same

deleted theorem set.sdiff_singleton_eq_same

deleted theorem set.sdiff_subset_sdiff

deleted theorem set.sdiff_union_same

added theorem set.sub_eq_diff

modified theorem set.subset_Union

modified theorem set.subset_sUnion_of_mem

added theorem set.union_Inter_left

added theorem set.union_Union_left

added theorem set.union_Union_right

deleted theorem set.union_distrib_Inter_left

added theorem set.union_eq_Union

deleted theorem set.union_of_subset_right

deleted theorem set.union_same_compl

deleted theorem set.union_sdiff_left

deleted theorem set.union_sdiff_right

deleted theorem set.union_sdiff_same

Modified linear_algebra/basic.lean

Modified logic/schroeder_bernstein.lean

Modified order/filter.lean

Modified order/galois_connection.lean