English
There is a fibration structure linking the game sum of two CutExpand relations to a single CutExpand relation via multiset addition.
Русский
Существует структура фибрации между игровой суммой двух CutExpand и единичной CutExpand через сложение мультисетов.
LaTeX
$$$\\text{Fibration} (\\mathrm{GameAdd}(\\mathrm{CutExpand}(r),\\mathrm{CutExpand}(r)))\\; (\\mathrm{CutExpand}(r))\\; (s \\mapsto s_1 + s_2)$$$
Lean4
theorem cutExpand_le_invImage_lex [DecidableEq α] [IsIrrefl α r] :
CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp :=
by
rintro s t ⟨u, a, hr, he⟩
replace hr := fun a' ↦ mt (hr a')
classical
refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
· apply_fun count b at he
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)] using he
· apply_fun count a at he
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)), add_zero] at he
exact he ▸ Nat.lt_succ_self _
