aesop
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ 0 < x u
no goals