α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ (#WType β) ≤ max (#α) ℵ₀
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ IsEmpty α → (#WType β) ≤ max (#α) ℵ₀
intro h
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ max (#α) ℵ₀
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ (#WType β) ≤ max (#α) ℵ₀
rw [Cardinal.mk_eq_zero (WType β)]
no goals
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
h : IsEmpty α
⊢ 0 ≤ max (#α) ℵ₀
exact zero_le _
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal := max (#α) ℵ₀
⊢ 1 ≤ ⨆ (a : α), m ^ (#β a)
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal := max (#α) ℵ₀
⊢ Order.succ 0 ≤ ⨆ (a : α), m ^ (#β a)
rw [succ_zero]
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ 1 ≤ ⨆ (a : α), m ^ (#β a)
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
hn : Nonempty α
m : Cardinal := max (#α) ℵ₀
⊢ 1 ≤ ⨆ (a : α), m ^ (#β a)
obtain ⟨a⟩ : Nonempty α := hn
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ 1 ≤ m ^ (#β a)
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ 1 ≤ ⨆ (a : α), m ^ (#β a)
refine' le_trans _ (le_ciSup (bddAbove_range.{u, u} _) a)
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ ?m.2512 ^ 0 ≤ m ^ (#β a)

α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ Cardinal
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ 1 ≤ m ^ (#β a)
rw [← power_zero]
no goals
case intro
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ ?m.2512 ^ 0 ≤ m ^ (#β a)

α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal := max (#α) ℵ₀
a : α
⊢ Cardinal
exact
  power_le_power_left
    (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) (zero_le _)