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