Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-27 09:03
caa86f12
View on Github →
feat: port Analysis.InnerProductSpace.LaxMilgram (
#4415
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
added
theorem
IsCoercive.antilipschitz
added
theorem
IsCoercive.bounded_below
added
theorem
IsCoercive.closed_range
added
def
IsCoercive.continuousLinearEquivOfBilin
added
theorem
IsCoercive.continuousLinearEquivOfBilin_apply
added
theorem
IsCoercive.ker_eq_bot
added
theorem
IsCoercive.range_eq_top
added
theorem
IsCoercive.unique_continuousLinearEquivOfBilin