You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Define preimage, then level set as a preimage with a symbol #467
Ezra asked on #461 whether a level set should have a symbol, and whether every definition needs one.
Decision (daytb): a definition gets a symbol only when the term recurs in formulas. A level set recurs, so it gets one, defined by its most literal meaning: the preimage of the single value c.
Plan, in small PRs:
mds: a "Preimage" def with an example (this repo).
macros: a preimage macro, and a level-set macro defined from it, plus the notation-choices entry.
mds: use the level-set macro in the level set def and example.
Activity
Write the level set as a preimage with the shared macro (#471)