Remix.run Logo
drdeca 2 days ago

It is quite common for a lemma to be needed to ensure that a definition is well-defined. The term “defi-lemma” exists for a reason.

As a simple example, suppose X is a set and r is a relation on X. If I define Y := X/r , the set of equivalence relations with respect to r, this implicitly assumes that the relation r is an equivalence relation.