α β : Type u
b c a : Cardinal
h : c < b
⊢ BddAbove (range fun y => a ^ ↑y)
α β : Type u
b c a : Cardinal
h : c < b
⊢ a ^ c ≤ a ^< b
refine le_ciSup (f := fun y : Iio b => a^y) ?_ ⟨c, h⟩
α β : Type u
b c a : Cardinal
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
α β : Type u
b c a : Cardinal
h : c < b
⊢ BddAbove (range fun y => a ^ ↑y)
rw [← image_eq_range]
no goals
α β : Type u
b c a : Cardinal
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
exact bddAbove_image.{u, u} _ bddAbove_Iio