Add Erdős Problem 1173 (set mappings on ω_{ω+1} under GCH)

[henrykmichalewski]

Formalizes Erdős Problem 1173 on set mappings and free sets on ω_{ω+1} under GCH.

Contents

• New IsSetMapping definition (a set mapping f : α → Set α with x ∉ f x and a size bound).
• New IsFreeSet definition (a subset pairwise disjoint from the mapping's images).
• The main open theorem statement for Problem 1173.
• Two proved auxiliary lemmas:
  • monotonicity of IsSetMapping in the size bound
  • an image-size bound for set mappings

Closes #1996

Assisted by Claude (Anthropic).