English
If α is infinite and β has at least two elements, then #(Finsupp α β) = max(|α|, |β|).
Русский
Если α бесконечен, а у β есть по меньшей мере два элемента, то #(Finsupp α β) = max(|α|, |β|).
LaTeX
$$$$ \\#(\\alpha \\to_{0} \\beta) = \\max\\{\\lvert \\alpha\\rvert,\\lvert \\beta\\rvert\\}. $$$$
Lean4
@[simp]
theorem mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] :
#(α →₀ β) = max (lift.{v} #α) (lift.{u} #β) := by
apply le_antisymm
·
calc
#(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
_ = #(α × β) := (mk_finset_of_infinite _)
_ = max (lift.{v} #α) (lift.{u} #β) := by rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp
· apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]
· obtain ⟨b, hb⟩ := exists_ne (0 : β)
exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
· inhabit α
exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩
