Theorem: SciLean.ContinuousLinearMap.mk'_eval (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R : Type u_1
inst✝⁶ : Semiring R
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module R X
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : AddCommMonoid Y
inst✝ : Module R Y
x : X
f : X → Y
hf : IsContinuousLinearMap R f
⊢ (mk' R f hf) x = f x
Tactic:
rfl
State after:
no goals