On Thu, 13 Jun 2019 03:51:00 -0700 (PDT), Benoit <[email protected]> wrote: > Continuing the discussion with Thierry and David: > > I would still use "exp" for theorems related to the exponential and "pow" > for theorems related to power functions. With "itg" for theorems related > to integrals, this would give "itgpow" for Jon's current "itexp". I would > also add these three lines to the table at "conventions". The main reason > is that "exp" is much more memorable than "ef"; this is more important to > me than strict consistency with the labels used for the definitions. > > If consistency with the definition labels has to be kept, and probably it > should, then I would use "df-expt" for exponentiation (currently "df-exp") > and "df-exp" for the exponential (currently "df-ef"). Overall, the complex > exponential is a more important object than exponentiation as defined in > set.mm (i.e. the function defined on \C \times \Z).
We are not *always* consistent with the definitions, but I think I think we should be "mostly consistent", have a reason to be inconsistent, and then *document* that inconsistency (e.g., in the small table). The consistency greatly eases searching, which is becoming more & more important over time now that we have so many proven theorems (a good problem to have!). We could change the labels to match the definitions, *or* we could change the definition names to match the preferred labels. The new proposed definition names make sense to me, and if they help others then great! --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1hbTqe-0006AI-Lo%40rmmprod07.runbox.
