Commit 2023-05-28 20:08 0f5133e2

View on Github →

feat: add Set.IccExtend_eq_self (#4454) Partial forward-port of leanprover-community/mathlib#19097 Also rename Set.Icc_extend_coe to Set.IccExtend_val.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

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

added theorem Set.IccExtend_eq_self

added theorem Set.IccExtend_val

deleted theorem Set.Icc_extend_coe

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/PathConnected.lean