α β ι : Type u
f : ι → Cardinal
hf : BddAbove (range f)
g : Cardinal → Cardinal
⊢ BddAbove (g '' range f)
α β ι : Type u
f : ι → Cardinal
hf : BddAbove (range f)
g : Cardinal → Cardinal
⊢ BddAbove (range (g ∘ f))
rw [range_comp]
no goals
α β ι : Type u
f : ι → Cardinal
hf : BddAbove (range f)
g : Cardinal → Cardinal
⊢ BddAbove (g '' range f)
exact bddAbove_image.{v,w} g hf