Commit 2022-05-23 01:49 9861db0d

feat(logic/hydra): termination of a hydra game (#14190)

• The added file logic/hydra.lean deals with the following version of the hydra game: each head of the hydra is labelled by an element in a type α, and when you cut off one head with label a, it grows back an arbitrary but finite number of heads, all labelled by elements smaller than a with respect to a well-founded relation r on α. We show that no matter how (in what order) you choose cut off the heads, the game always terminates, i.e. all heads will eventually be cut off. The proof follows https://mathoverflow.net/a/229084/3332, and the notion of fibration and the game_add relation on the product of two types arise in the proof.
• The results is used to show the well-foundedness of the intricate induction used to show that multiplication of games is well-defined on surreals, see Zulip discussion.
• One lemma add_singleton_eq_iff is added to data/multiset/basic.
• acc.trans_gen is added, closing a comment at lean#713.