English
Let f be a finitely supported function f: ι →₀ α, where α is a canonically ordered additive monoid with a bottom element and locally finite order. Then the number of functions g with g < f (in the pointwise order) equals the product over i in the support of f of (the number of elements ≤ f(i)) minus 1, i.e. |{g : g < f}| = ∏_{i ∈ supp(f)} (|Iic(f(i))| − 1).
Русский
Пусть f — конечно опорная функция f: ι →₀ α, где α — канонически упорядоченный добавочно-моноид с нулём и локально конечным порядком. Тогда число функций g с g < f (по покомпонентному порядку) равно произведению по i из опоры f величины |{x ∈ α : x ≤ f(i)}| − 1: |{g : g < f}| = ∏_{i ∈ supp(f)} (|Iic(f(i))| − 1).
LaTeX
$$$\\#(Iio f) = \\prod_{i \\in \\mathrm{supp}(f)} \\left( \\#\\bigl(Iic(f(i))\\bigr) - 1 \\right)$$$
Lean4
theorem card_Iio : #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1 := by rw [card_Iio_eq_card_Iic_sub_one, card_Iic]
