Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 18:07 9d01cb8b

View on Github →

refactor(algebra/lattice): use *experiment files, move set.lattice to .basic

Estimated changes

Modified algebra/lattice/basic.lean

modified theorem lattice.bot_inf_eq

modified theorem lattice.bot_le

modified theorem lattice.bot_sup_eq

modified theorem lattice.inf_bot_eq

modified theorem lattice.inf_eq_top_iff

modified theorem lattice.inf_idem

added theorem lattice.inf_le_left'

added theorem lattice.inf_le_right'

modified theorem lattice.inf_top_eq

added theorem lattice.le_bot_iff

modified theorem lattice.le_inf_iff

added theorem lattice.le_sup_left'

added theorem lattice.le_sup_right'

modified theorem lattice.le_top

modified theorem lattice.sup_bot_eq

modified theorem lattice.sup_eq_bot_iff

modified theorem lattice.sup_idem

modified theorem lattice.sup_le_iff

modified theorem lattice.sup_top_eq

modified theorem lattice.top_inf_eq

added theorem lattice.top_le_iff

modified theorem lattice.top_sup_eq

added theorem le_antisymm'

Deleted algebra/lattice/basic_experiment.lean

deleted theorem lattice.bot_inf_eq

deleted theorem lattice.bot_le

deleted theorem lattice.bot_sup_eq

deleted theorem lattice.bot_unique

deleted theorem lattice.eq_bot_iff

deleted theorem lattice.eq_top_iff

deleted def lattice.imp

deleted theorem lattice.inf_assoc

deleted theorem lattice.inf_bot_eq

deleted theorem lattice.inf_comm

deleted theorem lattice.inf_eq_top_iff

deleted theorem lattice.inf_idem

deleted theorem lattice.inf_le_inf

deleted theorem lattice.inf_le_left'

deleted theorem lattice.inf_le_left

deleted theorem lattice.inf_le_left_of_le

deleted theorem lattice.inf_le_right'

deleted theorem lattice.inf_le_right

deleted theorem lattice.inf_le_right_of_le

deleted theorem lattice.inf_of_le_left

deleted theorem lattice.inf_of_le_right

deleted theorem lattice.inf_sup_self

deleted theorem lattice.inf_top_eq

deleted theorem lattice.le_bot_iff

deleted theorem lattice.le_inf

deleted theorem lattice.le_inf_iff

deleted theorem lattice.le_inf_sup

deleted theorem lattice.le_of_inf_eq

deleted theorem lattice.le_of_sup_eq

deleted theorem lattice.le_sup_left'

deleted theorem lattice.le_sup_left

deleted theorem lattice.le_sup_left_of_le

deleted theorem lattice.le_sup_right'

deleted theorem lattice.le_sup_right

deleted theorem lattice.le_sup_right_of_le

deleted theorem lattice.le_top

deleted theorem lattice.neq_bot_of_le_neq_bot

deleted theorem lattice.sup_assoc

deleted theorem lattice.sup_bot_eq

deleted theorem lattice.sup_comm

deleted theorem lattice.sup_eq_bot_iff

deleted theorem lattice.sup_idem

deleted theorem lattice.sup_inf_le

deleted theorem lattice.sup_inf_self

deleted theorem lattice.sup_le

deleted theorem lattice.sup_le_iff

deleted theorem lattice.sup_le_sup

deleted theorem lattice.sup_of_le_left

deleted theorem lattice.sup_of_le_right

deleted theorem lattice.sup_top_eq

deleted theorem lattice.top_inf_eq

deleted theorem lattice.top_le_iff

deleted theorem lattice.top_sup_eq

deleted theorem lattice.top_unique

deleted theorem le_antisymm'

Modified algebra/lattice/bounded_lattice.lean

Deleted algebra/lattice/bounded_lattice_experiment.lean

deleted theorem lattice.monotone_and

deleted theorem lattice.monotone_or

Modified algebra/lattice/complete_boolean_algebra.lean

Modified algebra/lattice/complete_lattice.lean

added theorem lattice.foo'

added theorem lattice.foo

added theorem lattice.infi_le'

added theorem lattice.le_supr'

deleted theorem set.subset_union_left

deleted theorem set.subset_union_right

Deleted algebra/lattice/complete_lattice_experiment.lean

deleted theorem insert_def

deleted theorem insert_eq_of_mem

deleted theorem insert_of_has_insert

deleted theorem inter_def

deleted theorem inter_left_comm

deleted def lattice.Inf

deleted theorem lattice.Inf_empty

deleted theorem lattice.Inf_eq_infi

deleted theorem lattice.Inf_image

deleted theorem lattice.Inf_insert

deleted theorem lattice.Inf_le

deleted theorem lattice.Inf_le_Inf

deleted theorem lattice.Inf_le_Sup

deleted theorem lattice.Inf_le_iff

deleted theorem lattice.Inf_le_of_le

deleted theorem lattice.Inf_singleton

deleted theorem lattice.Inf_union

deleted theorem lattice.Inf_univ

deleted def lattice.Sup

deleted theorem lattice.Sup_empty

deleted theorem lattice.Sup_eq_supr

deleted theorem lattice.Sup_image

deleted theorem lattice.Sup_insert

deleted theorem lattice.Sup_inter_le

deleted theorem lattice.Sup_le

deleted theorem lattice.Sup_le_Sup

deleted theorem lattice.Sup_singleton

deleted theorem lattice.Sup_union

deleted theorem lattice.Sup_univ

deleted theorem lattice.foo'

deleted theorem lattice.foo

deleted def lattice.infi

deleted theorem lattice.infi_and

deleted theorem lattice.infi_comm

deleted theorem lattice.infi_congr_Prop

deleted theorem lattice.infi_const

deleted theorem lattice.infi_empty

deleted theorem lattice.infi_emptyset

deleted theorem lattice.infi_exists

deleted theorem lattice.infi_false

deleted theorem lattice.infi_inf_eq

deleted theorem lattice.infi_infi_eq_left

deleted theorem lattice.infi_infi_eq_right

deleted theorem lattice.infi_insert

deleted theorem lattice.infi_le'

deleted theorem lattice.infi_le

deleted theorem lattice.infi_le_infi2

deleted theorem lattice.infi_le_infi

deleted theorem lattice.infi_le_infi_const

deleted theorem lattice.infi_le_of_le

deleted theorem lattice.infi_or

deleted theorem lattice.infi_prod

deleted theorem lattice.infi_sigma

deleted theorem lattice.infi_singleton

deleted theorem lattice.infi_subtype

deleted theorem lattice.infi_sum

deleted theorem lattice.infi_true

deleted theorem lattice.infi_union

deleted theorem lattice.infi_unit

deleted theorem lattice.infi_univ

deleted theorem lattice.insert_of_has_insert

deleted theorem lattice.le_Inf

deleted theorem lattice.le_Inf_inter

deleted theorem lattice.le_Sup

deleted theorem lattice.le_Sup_iff

deleted theorem lattice.le_Sup_of_le

deleted theorem lattice.le_infi

deleted theorem lattice.le_infi_iff

deleted theorem lattice.le_supr'

deleted theorem lattice.le_supr

deleted theorem lattice.le_supr_of_le

deleted theorem lattice.monotone_Inf_of_monotone

deleted theorem lattice.monotone_Sup_of_monotone

deleted def lattice.supr

deleted theorem lattice.supr_and

deleted theorem lattice.supr_comm

deleted theorem lattice.supr_congr_Prop

deleted theorem lattice.supr_const

deleted theorem lattice.supr_empty

deleted theorem lattice.supr_emptyset

deleted theorem lattice.supr_exists

deleted theorem lattice.supr_false

deleted theorem lattice.supr_insert

deleted theorem lattice.supr_le

deleted theorem lattice.supr_le_iff

deleted theorem lattice.supr_le_supr2

deleted theorem lattice.supr_le_supr

deleted theorem lattice.supr_le_supr_const

deleted theorem lattice.supr_or

deleted theorem lattice.supr_prod

deleted theorem lattice.supr_sigma

deleted theorem lattice.supr_singleton

deleted theorem lattice.supr_subtype

deleted theorem lattice.supr_sum

deleted theorem lattice.supr_sup_eq

deleted theorem lattice.supr_supr_eq_left

deleted theorem lattice.supr_supr_eq_right

deleted theorem lattice.supr_true

deleted theorem lattice.supr_union

deleted theorem lattice.supr_unit

deleted theorem lattice.supr_univ

deleted theorem mem_insert_iff

deleted theorem mem_inter_eq

deleted theorem mem_set_of

deleted theorem mem_set_of_eq

deleted theorem mem_singleton

deleted theorem mem_singleton_iff

deleted theorem mem_union_eq

deleted theorem mem_univ_eq

deleted theorem nmem_set_of_eq

deleted theorem set_eq_def

deleted theorem set_of_false

deleted theorem singleton_def

deleted theorem singleton_eq_singleton_iff

deleted theorem subset_def

deleted theorem subset_insert

deleted theorem subset_univ

deleted theorem union_def

deleted theorem union_left_comm

Modified data/seq/wseq.lean

Modified data/set/basic.lean

added theorem set.bounded_forall_empty_iff

added theorem set.bounded_forall_image_iff

added theorem set.bounded_forall_image_of_bounded_forall

added theorem set.bounded_forall_insert_iff

added theorem set.compl_comp_compl

added theorem set.compl_compl

added theorem set.compl_compl_image

added theorem set.compl_empty

added theorem set.compl_eq_univ_diff

added theorem set.compl_inter

added theorem set.compl_inter_self

added theorem set.compl_union

added theorem set.compl_union_self

added theorem set.compl_univ

added theorem set.diff_eq

added theorem set.diff_subset

added theorem set.empty_def

modified theorem set.empty_inter

added theorem set.empty_ne_univ

modified theorem set.empty_subset

modified theorem set.empty_union

modified theorem set.eq_empty_of_forall_not_mem

modified theorem set.eq_empty_of_subset_empty

added theorem set.eq_of_mem_singleton

modified theorem set.eq_of_subset_of_subset

added def set.eq_on

added theorem set.eq_or_mem_of_mem_insert

added theorem set.eq_sep_of_subset

added theorem set.eq_univ_of_forall

added theorem set.eq_univ_of_univ_subset

added theorem set.eq_vimage_subtype_val_iff

added theorem set.exists_mem_of_ne_empty

modified theorem set.ext

added theorem set.fix_set_compl

added theorem set.forall_insert_of_forall

added theorem set.forall_not_of_sep_empty

added theorem set.forall_of_forall_insert

added theorem set.image_comp

added theorem set.image_empty

added theorem set.image_eq_image_of_eq_on

added theorem set.image_id

added theorem set.image_insert_eq

added theorem set.image_subset

added theorem set.image_subset_iff_subset_vimage

added theorem set.image_union

added theorem set.insert_comm

added theorem set.insert_def

added theorem set.insert_eq

added theorem set.insert_eq_of_mem

added theorem set.insert_ne_empty

added theorem set.insert_of_has_insert

modified theorem set.inter_assoc

modified theorem set.inter_comm

added theorem set.inter_compl_self

added theorem set.inter_def

added theorem set.inter_distrib_left

added theorem set.inter_distrib_right

modified theorem set.inter_empty

added theorem set.inter_eq_compl_compl_union_compl

added theorem set.inter_eq_self_of_subset_left

added theorem set.inter_eq_self_of_subset_right

added theorem set.inter_left_comm

added theorem set.inter_right_comm

modified theorem set.inter_self

added theorem set.inter_subset_inter

added theorem set.inter_subset_inter_left

added theorem set.inter_subset_inter_right

added theorem set.inter_subset_left

added theorem set.inter_subset_right

added theorem set.inter_univ

added theorem set.mem_compl

added theorem set.mem_compl_eq

added theorem set.mem_compl_iff

added theorem set.mem_diff

added theorem set.mem_diff_eq

added theorem set.mem_diff_iff

modified theorem set.mem_empty_eq

added theorem set.mem_image

added theorem set.mem_image_compl

added def set.mem_image_elim

added def set.mem_image_elim_on

added theorem set.mem_image_eq

added theorem set.mem_image_of_mem

added theorem set.mem_insert

added theorem set.mem_insert_iff

added theorem set.mem_insert_of_mem

added theorem set.mem_inter

added theorem set.mem_inter_eq

added theorem set.mem_inter_iff

added theorem set.mem_of_mem_diff

added theorem set.mem_of_mem_insert_of_ne

added theorem set.mem_of_mem_inter_left

added theorem set.mem_of_mem_inter_right

modified theorem set.mem_of_subset_of_mem

added theorem set.mem_or_mem_of_mem_union

added theorem set.mem_powerset

added theorem set.mem_powerset_iff

added theorem set.mem_sep

added theorem set.mem_sep_eq

added theorem set.mem_sep_iff

added theorem set.mem_set_of_eq

added theorem set.mem_singleton

added theorem set.mem_singleton_iff

added theorem set.mem_singleton_of_eq

added theorem set.mem_union.elim

added theorem set.mem_union_eq

added theorem set.mem_union_iff

added theorem set.mem_union_left

added theorem set.mem_union_right

added theorem set.mem_univ

added theorem set.mem_univ_eq

added theorem set.mem_univ_iff

added theorem set.mem_vimage_eq

added theorem set.mono_image

modified theorem set.ne_empty_of_mem

added theorem set.nmem_set_of_eq

added theorem set.nonempty_of_inter_nonempty_left

added theorem set.nonempty_of_inter_nonempty_right

modified theorem set.not_mem_empty

added theorem set.not_mem_of_mem_compl

added theorem set.not_mem_of_mem_diff

added theorem set.pair_eq_singleton

added def set.pairwise_on

added theorem set.sep_subset

added theorem set.set_eq_def

added theorem set.set_of_false

added theorem set.singleton_def

added theorem set.singleton_eq_singleton_iff

added theorem set.singleton_ne_empty

added theorem set.singleton_subset_iff

added theorem set.ssubset_def

added theorem set.ssubset_insert

added def set.strict_subset

modified theorem set.subset.antisymm

modified theorem set.subset.refl

modified theorem set.subset.trans

added theorem set.subset_def

added theorem set.subset_empty_iff

added theorem set.subset_insert

added theorem set.subset_inter

added theorem set.subset_of_mem_powerset

added theorem set.subset_union_left

added theorem set.subset_union_right

added theorem set.subset_univ

modified theorem set.union_assoc

modified theorem set.union_comm

added theorem set.union_compl_self

added theorem set.union_def

added theorem set.union_diff_cancel

added theorem set.union_distrib_left

added theorem set.union_distrib_right

modified theorem set.union_empty

added theorem set.union_eq_compl_compl_inter_compl

added theorem set.union_eq_self_of_subset_left

added theorem set.union_eq_self_of_subset_right

added theorem set.union_insert_eq

added theorem set.union_left_comm

added theorem set.union_right_comm

modified theorem set.union_self

added theorem set.union_subset

added theorem set.union_subset_iff

added theorem set.union_subset_union

added theorem set.univ_def

added theorem set.univ_inter

added def set.vimage

added theorem set.vimage_comp

added theorem set.vimage_compl

added theorem set.vimage_empty

added theorem set.vimage_id

added theorem set.vimage_image_eq

added theorem set.vimage_inter

added theorem set.vimage_mono

added theorem set.vimage_union

added theorem set.vimage_univ

Modified data/set/lattice.lean

deleted theorem set.bounded_forall_empty_iff

deleted theorem set.bounded_forall_image_iff

deleted theorem set.bounded_forall_image_of_bounded_forall

deleted theorem set.bounded_forall_insert_iff

deleted theorem set.compl_comp_compl

deleted theorem set.compl_compl

deleted theorem set.compl_compl_image

deleted theorem set.compl_empty

deleted theorem set.compl_eq_univ_diff

deleted theorem set.compl_inter

deleted theorem set.compl_inter_self

deleted theorem set.compl_union

deleted theorem set.compl_union_self

deleted theorem set.compl_univ

deleted theorem set.diff_eq

deleted theorem set.diff_subset

modified theorem set.disjoint_bot_left

modified theorem set.disjoint_bot_right

modified theorem set.disjoint_symm

deleted theorem set.empty_ne_univ

deleted theorem set.eq_of_mem_singleton

deleted def set.eq_on

deleted theorem set.eq_or_mem_of_mem_insert

deleted theorem set.eq_sep_of_subset

deleted theorem set.eq_univ_of_forall

deleted theorem set.eq_univ_of_univ_subset

deleted theorem set.eq_vimage_subtype_val_iff

deleted theorem set.exists_mem_of_ne_empty

deleted theorem set.fix_set_compl

deleted theorem set.forall_insert_of_forall

deleted theorem set.forall_not_of_sep_empty

deleted theorem set.forall_of_forall_insert

deleted theorem set.image_comp

deleted theorem set.image_empty

deleted theorem set.image_eq_image_of_eq_on

deleted theorem set.image_id

deleted theorem set.image_insert_eq

deleted theorem set.image_subset

deleted theorem set.image_subset_iff_subset_vimage

deleted theorem set.image_union

deleted theorem set.insert_comm

deleted theorem set.insert_def

deleted theorem set.insert_eq

deleted theorem set.insert_eq_of_mem

deleted theorem set.insert_ne_empty

deleted theorem set.insert_of_has_insert

modified theorem set.insert_sdiff_singleton

deleted theorem set.inter_compl_self

deleted theorem set.inter_def

deleted theorem set.inter_distrib_left

deleted theorem set.inter_distrib_right

deleted theorem set.inter_eq_compl_compl_union_compl

deleted theorem set.inter_eq_self_of_subset_left

deleted theorem set.inter_eq_self_of_subset_right

deleted theorem set.inter_left_comm

deleted theorem set.inter_right_comm

deleted theorem set.inter_subset_inter

deleted theorem set.inter_subset_inter_left

deleted theorem set.inter_subset_inter_right

deleted theorem set.inter_subset_left

deleted theorem set.inter_subset_right

deleted theorem set.inter_univ

deleted theorem set.mem_compl

deleted theorem set.mem_compl_eq

deleted theorem set.mem_compl_iff

deleted theorem set.mem_diff

deleted theorem set.mem_diff_eq

deleted theorem set.mem_diff_iff

deleted theorem set.mem_image

deleted theorem set.mem_image_compl

deleted def set.mem_image_elim

deleted def set.mem_image_elim_on

deleted theorem set.mem_image_eq

deleted theorem set.mem_image_of_mem

deleted theorem set.mem_insert

deleted theorem set.mem_insert_iff

deleted theorem set.mem_insert_of_mem

deleted theorem set.mem_inter

deleted theorem set.mem_inter_eq

deleted theorem set.mem_inter_iff

deleted theorem set.mem_of_mem_diff

deleted theorem set.mem_of_mem_insert_of_ne

deleted theorem set.mem_of_mem_inter_left

deleted theorem set.mem_of_mem_inter_right

deleted theorem set.mem_or_mem_of_mem_union

deleted theorem set.mem_powerset

deleted theorem set.mem_powerset_iff

deleted theorem set.mem_sep

deleted theorem set.mem_sep_eq

deleted theorem set.mem_sep_iff

deleted theorem set.mem_set_of

deleted theorem set.mem_set_of_eq

deleted theorem set.mem_singleton

deleted theorem set.mem_singleton_iff

deleted theorem set.mem_singleton_of_eq

deleted theorem set.mem_union.elim

deleted theorem set.mem_union_eq

deleted theorem set.mem_union_iff

deleted theorem set.mem_union_left

deleted theorem set.mem_union_right

deleted theorem set.mem_unionl

deleted theorem set.mem_unionr

deleted theorem set.mem_univ

deleted theorem set.mem_univ_eq

deleted theorem set.mem_univ_iff

deleted theorem set.mem_vimage_eq

deleted theorem set.mono_image

modified theorem set.monotone_vimage

deleted theorem set.nmem_set_of_eq

deleted theorem set.nonempty_of_inter_nonempty_left

deleted theorem set.nonempty_of_inter_nonempty_right

deleted theorem set.not_mem_of_mem_compl

deleted theorem set.not_mem_of_mem_diff

deleted theorem set.pair_eq_singleton

deleted def set.pairwise_on

modified theorem set.sdiff_singleton_eq_same

deleted theorem set.sep_subset

deleted theorem set.set_eq_def

deleted theorem set.set_of_false

deleted theorem set.singleton_def

deleted theorem set.singleton_eq_singleton_iff

deleted theorem set.singleton_ne_empty

deleted theorem set.singleton_subset_iff

deleted theorem set.ssubset_def

deleted theorem set.ssubset_insert

deleted def set.strict_subset

deleted theorem set.subset_def

deleted theorem set.subset_empty_iff

deleted theorem set.subset_insert

deleted theorem set.subset_inter

deleted theorem set.subset_of_mem_powerset

deleted theorem set.subset_univ

deleted theorem set.union_compl_self

deleted theorem set.union_def

deleted theorem set.union_diff_cancel

deleted theorem set.union_distrib_left

deleted theorem set.union_distrib_right

deleted theorem set.union_eq_compl_compl_inter_compl

deleted theorem set.union_eq_self_of_subset_left

deleted theorem set.union_eq_self_of_subset_right

deleted theorem set.union_insert_eq

deleted theorem set.union_left_comm

deleted theorem set.union_right_comm

modified theorem set.union_same_compl

modified theorem set.union_sdiff_same

deleted theorem set.union_subset

deleted theorem set.union_subset_iff

deleted theorem set.union_subset_union

deleted theorem set.univ_def

deleted theorem set.univ_inter

deleted def set.vimage

modified theorem set.vimage_Union

deleted theorem set.vimage_comp

deleted theorem set.vimage_compl

deleted theorem set.vimage_empty

deleted theorem set.vimage_id

deleted theorem set.vimage_image_eq

deleted theorem set.vimage_inter

deleted theorem set.vimage_mono

modified theorem set.vimage_sUnion

deleted theorem set.vimage_union

deleted theorem set.vimage_univ

Deleted tests/finish_set_basic.lean

deleted theorem set.bounded_forall_empty_iff

deleted theorem set.bounded_forall_image_iff

deleted theorem set.bounded_forall_image_of_bounded_forall

deleted theorem set.bounded_forall_insert_iff

deleted theorem set.compl_comp_compl

deleted theorem set.compl_compl

deleted theorem set.compl_compl_image

deleted theorem set.compl_empty

deleted theorem set.compl_eq_univ_diff

deleted theorem set.compl_inter

deleted theorem set.compl_inter_self

deleted theorem set.compl_union

deleted theorem set.compl_union_self

deleted theorem set.compl_univ

deleted theorem set.diff_eq

deleted theorem set.diff_subset

deleted theorem set.empty_def

deleted theorem set.empty_ne_univ

deleted theorem set.eq_of_mem_singleton

deleted def set.eq_on

deleted theorem set.eq_or_mem_of_mem_insert

deleted theorem set.eq_sep_of_subset

deleted theorem set.eq_univ_of_forall

deleted theorem set.eq_univ_of_univ_subset

deleted theorem set.exists_mem_of_ne_empty

deleted theorem set.fix_set_compl

deleted theorem set.forall_insert_of_forall

deleted theorem set.forall_not_of_sep_empty

deleted theorem set.forall_of_forall_insert

deleted theorem set.image_comp

deleted theorem set.image_empty

deleted theorem set.image_eq_image_of_eq_on

deleted theorem set.image_id

deleted theorem set.image_insert_eq

deleted theorem set.image_subset

deleted theorem set.image_union

deleted theorem set.insert_comm

deleted theorem set.insert_def

deleted theorem set.insert_eq

deleted theorem set.insert_eq_of_mem

deleted theorem set.insert_ne_empty

deleted theorem set.insert_of_has_insert

deleted theorem set.inter_compl_self

deleted theorem set.inter_def

deleted theorem set.inter_distrib_left

deleted theorem set.inter_distrib_right

deleted theorem set.inter_eq_compl_compl_union_compl

deleted theorem set.inter_eq_self_of_subset_left

deleted theorem set.inter_eq_self_of_subset_right

deleted theorem set.inter_left_comm

deleted theorem set.inter_right_comm

deleted theorem set.inter_subset_inter_left

deleted theorem set.inter_subset_inter_right

deleted theorem set.inter_subset_left

deleted theorem set.inter_subset_right

deleted theorem set.inter_univ

deleted theorem set.mem_compl

deleted theorem set.mem_compl_eq

deleted theorem set.mem_compl_iff

deleted theorem set.mem_diff

deleted theorem set.mem_diff_eq

deleted theorem set.mem_diff_iff

deleted theorem set.mem_image

deleted theorem set.mem_image_compl

deleted def set.mem_image_elim

deleted def set.mem_image_elim_on

deleted theorem set.mem_image_eq

deleted theorem set.mem_image_of_mem

deleted theorem set.mem_insert

deleted theorem set.mem_insert_iff

deleted theorem set.mem_insert_of_mem

deleted theorem set.mem_inter

deleted theorem set.mem_inter_eq

deleted theorem set.mem_inter_iff

deleted theorem set.mem_of_mem_diff

deleted theorem set.mem_of_mem_insert_of_ne

deleted theorem set.mem_of_mem_inter_left

deleted theorem set.mem_of_mem_inter_right

deleted theorem set.mem_or_mem_of_mem_union

deleted theorem set.mem_powerset

deleted theorem set.mem_powerset_iff

deleted theorem set.mem_sep

deleted theorem set.mem_sep_eq

deleted theorem set.mem_sep_iff

deleted theorem set.mem_set_of

deleted theorem set.mem_singleton

deleted theorem set.mem_singleton_iff

deleted theorem set.mem_singleton_of_eq

deleted theorem set.mem_union.elim

deleted theorem set.mem_union_eq

deleted theorem set.mem_union_iff

deleted theorem set.mem_union_left

deleted theorem set.mem_union_right

deleted theorem set.mem_unionl

deleted theorem set.mem_unionr

deleted theorem set.mem_univ

deleted theorem set.mem_univ_eq

deleted theorem set.mem_univ_iff

deleted theorem set.nonempty_of_inter_nonempty_left

deleted theorem set.nonempty_of_inter_nonempty_right

deleted theorem set.not_mem_of_mem_compl

deleted theorem set.not_mem_of_mem_diff

deleted theorem set.pair_eq_singleton

deleted theorem set.sep_subset

deleted theorem set.set_eq_def

deleted theorem set.singleton_def

deleted theorem set.singleton_ne_empty

deleted def set.strict_subset

deleted theorem set.subset_def

deleted theorem set.subset_empty_iff

deleted theorem set.subset_insert

deleted theorem set.subset_inter

deleted theorem set.subset_of_mem_powerset

deleted theorem set.subset_univ

deleted theorem set.union_compl_self

deleted theorem set.union_def

deleted theorem set.union_diff_cancel

deleted theorem set.union_distrib_left

deleted theorem set.union_distrib_right

deleted theorem set.union_eq_compl_compl_inter_compl

deleted theorem set.union_eq_self_of_subset_left

deleted theorem set.union_eq_self_of_subset_right

deleted theorem set.union_left_comm

deleted theorem set.union_right_comm

deleted theorem set.union_subset

deleted theorem set.univ_def

deleted theorem set.univ_inter

Modified theories/set_theory.lean

Modified topology/continuity.lean

Modified topology/topological_space.lean