fun_prop (disch:=aesop)
R✝ : Type ?u.25096
C : Type ?u.25095
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.25105
inst✝⁴ : Vec C W✝
U✝ : Type ?u.25128
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.25150
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), x u ≠ 0
u : U
⊢ HasAdjDiffAt R (fun u => log (x u)) u
no goals