Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 06:13 5cb17dd1

View on Github →

refactor(logic/is_empty): tag is_empty.forall_iff and is_empty.exists_iff as simp (#14660) We tag the lemmas forall_iff and exists_iff on empty types as simp. We remove forall_pempty, exists_pempty, forall_false_left, and exists_false_left due to being redundant.

Estimated changes

modified theorem dite_eq_iff
modified theorem dite_eq_left_iff
modified theorem dite_eq_right_iff
deleted theorem exists_false_left
deleted theorem exists_pempty
deleted theorem forall_false_left
deleted theorem forall_pempty
modified theorem is_empty.exists_iff
modified theorem is_empty.forall_iff