. fun_trans; fun_prop
case locally_diffeo
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_3
inst✝⁶ : Vec K Y
Z : Type ?u.9828
inst✝⁵ : Vec K Z
W : Type ?u.9839
inst✝⁴ : Vec K W
ι : Type ?u.9850
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.9877
inst✝ : (i : ι) → Vec K (E i)
y : Y
f : X → Y
hf : Diffeomorphism K f
bijective✝ : Function.Bijective f
differentiable✝ : CDifferentiable K f
locally_diffeo✝ : ∀ (x : X), Function.Bijective (cderiv K f x)
⊢ ∀ (x : X), Function.Bijective (cderiv K (fun x => y + f x) x)
no goals