Theorem IsCoercive.bounded_below

Modification history

2023-05-27 09:03

Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean

feat: port Analysis.InnerProductSpace.LaxMilgram (#4415)

Added IsCoercive.bounded_below View on Github →