English
Let I be an infinite index set and (c_i) a family of cardinals with c_i ≥ 2 for all i in I, and lift(c_i) ≤ lift(|I|) for all i. Then the Cartesian product ∏_{i∈I} c_i equals 2^{|I|}.
Русский
Пусть I — бесконечный набор индексов, и для каждого i∈I дано кардинальное число c_i, удовлетворяющее c_i ≥ 2 и lift(c_i) ≤ lift(|I|). Тогда произведение по i∈I c_i равно 2^{|I|}.
LaTeX
$$$ \\Bigl(\\forall i:\\, I,\\, 2 \\le c(i)\\Bigr) \\land \\Bigl(\\forall i:\\, I,\\, c(i) \\le |I|\\Bigr) \\implies \\prod_{i \\in I} c(i) = 2^{|I|}$$$
Lean4
theorem prod_eq_two_power {ι : Type u} [Infinite ι] {c : ι → Cardinal.{v}} (h₁ : ∀ i, 2 ≤ c i)
(h₂ : ∀ i, lift.{u} (c i) ≤ lift.{v} #ι) : prod c = 2 ^ lift.{v} #ι :=
by
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
apply le_antisymm
· refine (prod_le_prod _ _ h₂).trans_eq ?_
rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
· rw [← prod_const', lift_prod]
refine prod_le_prod _ _ fun i => ?_
rw [lift_two, ← lift_two.{u, v}, lift_le]
exact h₁ i
