Commit 2025-03-25 15:14 f832b449

View on Github →

chore: an injective bounded linear operator has closed range iff it is anti-Lipschitz (#23175) And make the argument f of ContinuousLinearMap.equivRange implicit, as the explicit hypotheses hf and hclo mention f.

Estimated changes

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

added theorem ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range

modified theorem ContinuousLinearMap.coe_equivRange

modified theorem ContinuousLinearMap.coe_linearMap_equivRange

added theorem ContinuousLinearMap.equivRange_symm_apply

added theorem ContinuousLinearMap.equivRange_symm_toLinearEquiv

added theorem ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective