Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-03 20:55 8faac5f8

View on Github →

refactor(logic/basic): refactor logic theorems

Estimated changes

Modified algebra/big_operators.lean

deleted theorem exists_false

Modified data/finset/basic.lean

deleted theorem finset.eq_of_mem_singleton

deleted theorem finset.eq_of_singleton_eq

modified theorem finset.mem_singleton

deleted theorem finset.mem_singleton_iff

deleted theorem finset.mem_singleton_of_eq

added theorem finset.mem_singleton_self

added theorem finset.singleton_inj

added theorem finset.subset_iff

deleted theorem finset.subset_of_forall

deleted theorem or_self_or

deleted theorem perm_insert_cons_of_not_mem

Modified data/finset/fold.lean

modified theorem finset.fold_congr

modified theorem list.map_congr

Modified data/list/basic.lean

Modified data/list/comb.lean

Modified data/list/perm.lean

Modified data/list/set.lean

Modified data/seq/seq.lean

Modified data/set/basic.lean

added theorem set.ball_empty_iff

added theorem set.ball_image_iff

added theorem set.ball_image_of_ball

added theorem set.ball_insert_iff

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

added theorem set.mem_union

deleted theorem set.mem_union_iff

added theorem set.not_not_mem

deleted theorem set.not_not_mem_iff

Modified data/set/lattice.lean

Modified logic/basic.lean

added theorem and.imp_left

added theorem and.imp_right

deleted theorem and_distrib

deleted theorem and_distrib_right

modified theorem and_iff_not_or_not

added theorem and_imp

deleted theorem and_imp_iff

deleted theorem and_implies_iff

deleted theorem and_implies_left

deleted theorem and_implies_right

deleted theorem and_not_of_not_implies

deleted theorem and_of_and_of_imp_left

deleted theorem and_of_and_of_imp_right

deleted theorem and_of_and_of_implies_of_implies

added theorem and_or_distrib_left

added theorem and_or_distrib_right

added theorem ball.imp_left

added theorem ball.imp_right

added theorem ball_and_distrib

added theorem ball_congr

added theorem ball_of_forall

added theorem ball_true_iff

added theorem bex.elim

added theorem bex.imp_left

added theorem bex.imp_right

added theorem bex.intro

added theorem bex_congr

added theorem bex_def

added theorem bex_imp_distrib

added theorem bex_of_exists

added theorem bex_or_distrib

deleted theorem bexists.elim

deleted theorem bexists.intro

deleted theorem bexists_congr

deleted theorem bexists_def

deleted theorem bexists_implies_distrib

deleted theorem bexists_implies_of_bforall_implies

deleted theorem bexists_not_of_not_bforall

deleted theorem bexists_of_bexists

deleted theorem bexists_of_exists

deleted theorem bexists_or_distrib

deleted theorem bforall_and_distrib

deleted theorem bforall_congr

deleted theorem bforall_implies_of_bexists_implies

deleted theorem bforall_not_of_not_bexists

deleted theorem bforall_of_bforall

deleted theorem bforall_of_forall

deleted theorem bforall_true_iff

deleted theorem classical.bexists_not_of_not_bforall

deleted theorem classical.exists_not_of_not_forall

added theorem classical.not_ball

deleted theorem classical.not_bforall_iff_bexists_not

added theorem classical.not_forall

deleted theorem classical.not_forall_iff

added def decidable_of_iff'

added def decidable_of_iff

modified theorem eq_iff_le_and_le

added theorem exists_const

added theorem exists_eq'

added theorem exists_eq

added theorem exists_eq_right'

added theorem exists_eq_right

added theorem exists_false

added theorem exists_imp_distrib

deleted theorem exists_implies_distrib

deleted theorem exists_implies_of_forall_implies

deleted theorem exists_not_of_not_forall

added theorem exists_of_bex

deleted theorem exists_of_bexists

modified theorem exists_of_exists

modified theorem exists_or_distrib

deleted theorem exists_p_iff_p

added theorem exists_prop

deleted theorem exists_prop_iff

added theorem exists_swap

modified theorem forall_and_distrib

added theorem forall_const

added theorem forall_eq'

modified theorem forall_eq

deleted theorem forall_implies_of_exists_implies

added theorem forall_of_ball

deleted theorem forall_of_bforall

modified theorem forall_of_forall

added theorem forall_or_of_or_forall

deleted theorem forall_p_iff_p

added theorem forall_swap

added theorem forall_true_iff'

modified theorem forall_true_iff

added theorem iff_def'

modified theorem iff_def

added theorem iff_false_left

added theorem iff_false_right

added theorem iff_not_comm

added theorem iff_of_false

added theorem iff_of_true

added theorem iff_true_left

added theorem iff_true_right

added theorem imp_and_distrib

added theorem imp_false

added theorem imp_iff_not_or

added theorem imp_iff_right

added theorem imp_intro

added theorem imp_not_comm

added theorem imp_of_not_or

added theorem imp_self

added theorem imp_true_iff

deleted theorem implies_and_iff

deleted theorem implies_false_iff

deleted theorem implies_iff

deleted theorem implies_iff_not_or

deleted theorem implies_intro

deleted theorem implies_of_not_or

deleted theorem implies_self

added theorem not.elim

added theorem not.imp_symm

added theorem not_and_distrib'

added theorem not_and_distrib

deleted theorem not_and_iff

added theorem not_and_iff_imp'

added theorem not_and_iff_imp

deleted theorem not_and_iff_imp_not

deleted theorem not_and_not_of_not_or

added theorem not_ball

added theorem not_ball_of_bex_not

added theorem not_bex

deleted theorem not_bexists_iff_bforall_not

deleted theorem not_bexists_of_bforall_not

deleted theorem not_bforall_iff_bexists_not

deleted theorem not_bforall_of_bexists_not

added theorem not_exists

deleted theorem not_exists_iff

added theorem not_exists_not

added theorem not_forall

deleted theorem not_forall_iff

added theorem not_forall_not

modified theorem not_forall_of_exists_not

added theorem not_iff_comm

added theorem not_iff_not

added theorem not_imp

added theorem not_imp_comm

deleted theorem not_imp_iff_not_imp

added theorem not_imp_not

added theorem not_imp_of_and_not

deleted theorem not_implies_iff

deleted theorem not_implies_of_and_not

added theorem not_not

deleted theorem not_not_elim

deleted theorem not_not_iff

added theorem not_not_of_not_imp

deleted theorem not_not_of_not_implies

added theorem not_of_not_imp

deleted theorem not_of_not_implies

added theorem not_or_distrib

deleted theorem not_or_iff

deleted theorem not_or_not_of_not_and'

deleted theorem not_or_not_of_not_and

added theorem not_or_of_imp

deleted theorem not_or_of_implies

deleted theorem not_or_of_not_and_not

added theorem of_not_imp

deleted theorem of_not_implies

added theorem of_not_not

added theorem or_and_distrib_left

added theorem or_and_distrib_right

deleted theorem or_distrib

deleted theorem or_distrib_right

modified theorem or_iff_not_and_not

added theorem or_iff_not_imp_left

added theorem or_iff_not_imp_right

deleted theorem or_iff_or

added theorem or_imp_distrib

deleted theorem or_imp_iff_and_imp

deleted theorem or_implies_distrib

deleted theorem or_of_not_implies'

deleted theorem or_of_not_implies

added theorem or_of_or_of_imp_left

added theorem or_of_or_of_imp_of_imp

added theorem or_of_or_of_imp_right

deleted theorem or_of_or_of_implies_left

deleted theorem or_of_or_of_implies_of_implies

deleted theorem or_of_or_of_implies_right

deleted theorem or_resolve_left

deleted theorem or_resolve_right

modified theorem prod.exists

modified theorem prod.forall

modified theorem prod.mk.inj_iff

deleted theorem {u

deleted theorem {u}

Modified order/bounds.lean

Modified order/filter.lean

Modified order/zorn.lean

Modified tactic/finish.lean

modified theorem auto.classical.implies_iff_not_or

modified theorem auto.not_and_eq

modified theorem auto.not_exists_eq

modified theorem auto.not_forall_eq

modified theorem auto.not_implies_eq

modified theorem auto.not_not_eq

modified theorem auto.not_or_eq

Modified topology/continuity.lean

Modified topology/ennreal.lean

Modified topology/measurable_space.lean

Modified topology/metric_space.lean

modified theorem continuous_dist'

modified theorem continuous_dist

modified theorem dist_comm

modified theorem dist_eq_zero_iff

modified theorem dist_nonneg

modified theorem dist_pos_of_ne

modified theorem dist_self

modified theorem dist_triangle

modified theorem eq_of_dist_eq_zero

modified theorem eq_of_forall_dist_le

modified theorem exists_subtype

modified theorem ne_of_dist_pos

modified theorem open_ball_subset_open_ball_of_le

modified theorem tendsto_dist

modified theorem uniform_continuous_dist'

modified theorem uniform_continuous_dist

modified theorem uniformity_dist'

modified theorem uniformity_dist

modified theorem zero_eq_dist_iff

Modified topology/real.lean

Modified topology/topological_space.lean

Modified topology/topological_structures.lean

Modified topology/uniform_space.lean