Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 22:35 dc57de22

View on Github →

feat(logic/basic): When a dependent If-Then-Else is not one of its arguments (#10924) This is the dependent version of #10800.

Estimated changes

added theorem dite_eq_iff
added theorem dite_eq_left_iff
added theorem dite_eq_or_eq
added theorem dite_eq_right_iff
added theorem dite_ne_left_iff
added theorem dite_ne_right_iff
added theorem exists_iff_of_forall
modified theorem ite_eq_iff
modified theorem ite_eq_left_iff
modified theorem ite_eq_right_iff
modified theorem ite_ne_left_iff
modified theorem ite_ne_right_iff
added theorem not_ne_iff