Commit 2023-05-06 08:29 cab52563

View on Github →

chore: fix names (#3812) Forward-port leanprover-community/mathlib#18921 and leanprover-community/mathlib#18924

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Basic.lean

added theorem abs_norm

deleted theorem abs_norm_eq_norm

Modified Mathlib/Data/Set/Intervals/Monotone.lean

added theorem StrictMonoOn.Ici_le_id

deleted theorem StrictMonoOn.Iic_le_id

added theorem strictAntiOn_Ici_of_lt_pred

deleted theorem strictAntiOn_Iic_of_lt_pred

added theorem strictMonoOn_Ici_of_pred_lt

deleted theorem strictMonoOn_Iic_of_pred_lt