Email Gateway (Aug 22 2022 at 13:03): Email Gateway (Aug 22 2022 at 13:03):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi
please I want to know if I used for example the definition: "setL2 f A" in
L2_norm.thy , so does this apply all lemmas inside the theory file as
setL2_cong and setL2_triangle_ineq and so on or I have to apply each lemma
in my file?
and another question: in setL2 f A = sqrt (∑i∈A. (f i)⇧2), how can I
substitute i as the definition just include f and A?
Many thanks in advance
Omar
Last updated: Nov 21 2024 at 12:39 UTC