Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Wellfounded.measure v Sigma_Algebra.measure

Email Gateway (Aug 19 2022 at 17:31):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

I imported the measure theory library and then wanted to prove
termination of a function using ‘apply (relation "measure …")’ and
noticed that this measure is now interpreted as Sigma_Algebra.measure,
i.e. the measure function belonging to a measure space, not as
Wellfounded.measure as intended.

I therefore propose to rename one of them, probably Wellfounded.measure.
What do you think?

Cheers,

Manuel

Email Gateway (Aug 19 2022 at 17:31):

From: Tobias Nipkow <nipkow@in.tum.de>
Both are established names. I see no harm in writing Wellfounded.measure in your
context.

Tobias
smime.p7s

Last updated: Apr 25 2024 at 04:18 UTC