ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (c i)) = lift (2 ^ (#ι))
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ prod c = 2 ^ lift (#ι)
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (c i)) ≤ lift (2 ^ (#ι))

case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ lift (2 ^ (#ι)) ≤ prod fun i => lift (c i)
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (c i)) = lift (2 ^ (#ι))
apply le_antisymm
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (#ι)) = lift (2 ^ (#ι))
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (c i)) ≤ lift (2 ^ (#ι))
refine' (prod_le_prod _ _ h₂).trans_eq _
no goals
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift (#ι)) = lift (2 ^ (#ι))
rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift 2) ≤ prod fun i => lift (c i)
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ lift (2 ^ (#ι)) ≤ prod fun i => lift (c i)
rw [← prod_const', lift_prod]
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
i : ι
⊢ lift 2 ≤ lift (c i)
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
⊢ (prod fun i => lift 2) ≤ prod fun i => lift (c i)
refine' prod_le_prod _ _ fun i => _
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
i : ι
⊢ 2 ≤ c i
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
i : ι
⊢ lift 2 ≤ lift (c i)
rw [lift_two, ← lift_two.{u, v}, lift_le]
no goals
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift (c i) ≤ lift (#ι)
i : ι
⊢ 2 ≤ c i
exact h₁ i