mk_finsupp_of_infinite — Mathlib

English

For α infinite and β with a zero, the cardinality is the maximum of the lifted cardinals: #(Finsupp α β) = max (lift |α|) (lift |β|).

Русский

Если α бесконечен и β имеет ноль, то #(Finsupp α β) = max (lift |α|) (lift |β|).

LaTeX

$$$$ \\#(\\alpha \\to_{0} \\beta) = \\max(\\operatorname{lift} \\lvert \\alpha \\rvert, \\operatorname{lift} \\lvert \\beta \\rvert). $$$$

Lean4

theorem mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] : #(α →₀ β) = max #α #β := by simp

Похожие утверждения