In mathematics, a binary relation is called well-founded (or wellfounded or foundational) on a class if every non-empty subset has a minimal element with respect to , that is, an element not related by (for instance, " is not smaller than ") for any . In other words, a relation is well founded if Some authors include an extra condition that is set-like, i.e., that the elements less than any given element form a set. Equivalently, assuming the axiom of dependent choice, a relation is well-founded when it contains no infinite descending chains, which can be proved when there is no infinite sequence of elements of such that for every natural number . In order theory, a partial order is called well-founded if the corresponding strict order is a well-founded relation. If the order is a total order then it is called a well-order. In set theory, a set is called a well-founded set if the set membership relation is well-founded on the transitive closure of . The axiom of regularity, which is one of the axioms of Zermelo–Fraenkel set theory, asserts that all sets are well-founded. A relation is converse well-founded, upwards well-founded or Noetherian on , if the converse relation is well-founded on . In this case is also said to satisfy the ascending chain condition. In the context of rewriting systems, a Noetherian relation is also called terminating. Induction and recursion An important reason that well-founded relations are interesting is because a version of transfinite induction can be used on them: if () is a well-founded relation, is some property of elements of , and we want to show that holds for all elements of , it suffices to show that: If is an element of and is true for all such that , then must also be true. That is, Well-founded induction is sometimes called Noetherian induction, after Emmy Noether. On par with induction, well-founded relations also support construction of objects by transfinite recursion. Let be a set-like well-founded relation and a function that assigns an object to each pair of an element and a function on the initial segment of . Then there is a unique function such that for every , That is, if we want to construct a function on , we may define using the values of for . As an example, consider the well-founded relation , where is the set of