Thank you for the hint to Norm's "rules of thumbs":
*Definitions are at the heart of achieving simplicity. While developing set.mm <http://set.mm>, two rules of thumb that evolved in my own work were (1) there shouldn't be two definitions that mean almost the same thing and (2) definitions shouldn't be introduced unless there is an actual need in the work at hand. Maybe I should add (3), don't formally define something that doesn't help proofs and can be stated simply in English in a theorem's comment. * So my suggestion would break rule (1) and maybe also rule (3)*. *But are the "problems" (reasons for the rules) mentioned by Norm also problems for 0o? Are really a lot of conversions needed as long as we are in the context of ordinal numbers? What is bad about a theorem ` 0o e. 1o ` which is identical with ` 0lt1o $p |- (/) e. 1o $= `? Would not even the definition of 1o break these rules, because 1o is identical with `{ (/) }`(see ~ df1o2), which is also often used outside the context of ordinal numbers? -- 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/596b7dbc-6c9f-4885-9170-d37281b918bfn%40googlegroups.com.
