Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-11 17:57 218c1dd3

View on Github →

algebra/lattice/filter: cleanup move theorems to appropriate places

Estimated changes

Modified algebra/lattice/boolean_algebra.lean

added theorem lattice.eq_of_sup_eq_inf_eq

added theorem lattice.inf_eq_bot_iff_le_compl

Modified algebra/lattice/filter.lean

deleted theorem Union_subset_Union2

deleted theorem Union_subset_Union

deleted theorem Union_subset_Union_const

deleted theorem bind_assoc

deleted theorem classical.cases

deleted theorem compl_image_set_of

deleted theorem diff_empty

deleted theorem diff_neq_empty

deleted theorem eq_of_sup_eq_inf_eq

deleted theorem false_neq_true

deleted theorem implies_implies_true_iff

deleted theorem inf_eq_bot_iff_le_compl

deleted theorem map_bind

deleted theorem neg_subset_neg_iff_subset

deleted theorem not_not_mem_iff

deleted theorem not_or_iff_implies

deleted theorem prod.fst_swap

deleted theorem prod.mk.eta

deleted theorem prod.snd_swap

deleted def prod.swap

deleted theorem prod.swap_prod_mk

deleted theorem prod.swap_swap

deleted theorem prod.swap_swap_eq

deleted theorem pure_seq_eq_map

deleted theorem sUnion_eq_Union

deleted theorem sUnion_mono

deleted theorem seq_bind_eq

deleted theorem seq_eq_bind_map

deleted theorem set.bind_def

deleted theorem set.diff_right_antimono

deleted theorem set.fmap_eq_image

deleted theorem set.image_Union

deleted theorem set.image_inter

deleted theorem set.image_singleton

deleted theorem set.image_swap_eq_preimage_swap

deleted theorem set.image_swap_prod

deleted theorem set.mem_prod_eq

deleted theorem set.mem_seq_iff

deleted theorem set.monotone_prod

deleted theorem set.ne_empty_iff_exists_mem

deleted theorem set.not_eq_empty_iff_exists

deleted theorem set.preimage_set_of_eq

deleted theorem set.prod_image_image_eq

deleted theorem set.prod_inter_prod

deleted theorem set.prod_mk_mem_set_prod_eq

deleted theorem set.prod_mono

deleted theorem set.prod_neq_empty_iff

deleted theorem set.prod_preimage_eq

deleted theorem set.prod_singleton_singleton

deleted theorem set.set_of_mem_eq

deleted theorem set.univ_eq_true_false

deleted theorem singleton_neq_emptyset

Created category/basic.lean

added theorem bind_assoc

added theorem map_bind

added theorem pure_seq_eq_map

added theorem seq_bind_eq

added theorem seq_eq_bind_map

Created data/prod.lean

added theorem prod.fst_swap

added theorem prod.mk.eta

added theorem prod.snd_swap

added def prod.swap

added theorem prod.swap_prod_mk

added theorem prod.swap_swap

added theorem prod.swap_swap_eq

Modified data/set/basic.lean

added theorem set.compl_image_set_of

added theorem set.compl_subset_of_compl_subset

added theorem set.diff_empty

added theorem set.diff_neq_empty

added theorem set.diff_right_antimono

added theorem set.diff_subset_diff

added theorem set.image_inter

added theorem set.image_singleton

added theorem set.mem_of_mem_of_subset

added theorem set.ne_empty_iff_exists_mem

added theorem set.not_eq_empty_iff_exists

added theorem set.not_not_mem_iff

added theorem set.preimage_set_of_eq

added theorem set.set_of_mem_eq

modified theorem set.singleton_ne_empty

added theorem set.univ_eq_true_false

Modified data/set/default.lean

Modified data/set/lattice.lean

added theorem set.Union_subset_Union2

added theorem set.Union_subset_Union

added theorem set.Union_subset_Union_const

added theorem set.bind_def

added theorem set.compl_subset_compl_iff_subset

added theorem set.fmap_eq_image

added theorem set.image_Union

added theorem set.mem_seq_iff

added theorem set.sUnion_eq_Union

added theorem set.sUnion_mono

added theorem set.univ_subtype

Created data/set/prod.lean

added theorem set.image_swap_eq_preimage_swap

added theorem set.image_swap_prod

added theorem set.mem_prod_eq

added theorem set.monotone_prod

added theorem set.prod_image_image_eq

added theorem set.prod_inter_prod

added theorem set.prod_mk_mem_set_prod_eq

added theorem set.prod_mono

added theorem set.prod_neq_empty_iff

added theorem set.prod_preimage_eq

added theorem set.prod_singleton_singleton

Modified logic/basic.lean

added theorem classical.cases

added theorem false_neq_true

added theorem not_and_iff_imp_not

added theorem {u

Modified topology/topological_space.lean

deleted theorem compl_subset_of_compl_subset

deleted theorem diff_subset_diff

deleted theorem mem_of_mem_of_subset

deleted theorem not_and_iff_imp_not

deleted theorem univ_subtype

Modified topology/uniform_space.lean