Commit 2024-05-05 09:43 ff35083c

View on Github →

feat: clean-up Topology.Order.IntermediateValue (#12403)

Also add variants of exists_apply_eq_apply['] for binary and ternary functions as simp-lemmas.
Remove note on exists_apply_eq_apply' that no longer applies.

Estimated changes

Modified Mathlib/Logic/Basic.lean

added theorem exists_apply_eq_apply2'

added theorem exists_apply_eq_apply2

added theorem exists_apply_eq_apply3'

added theorem exists_apply_eq_apply3

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/Topology/Order/IntermediateValue.lean