α β : Type u
ι : Type v
ι' : Type v'
f : ι → Cardinal
f' : ι' → Cardinal
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift (f i) ≤ lift (f' (g i))
⊢ (⨆ (i : ι), lift (f i)) ≤ ⨆ (i : ι'), lift (f' i)
α β : Type u
ι : Type v
ι' : Type v'
f : ι → Cardinal
f' : ι' → Cardinal
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift (f i) ≤ lift (f' (g i))
⊢ lift (iSup f) ≤ lift (iSup f')
rw [lift_iSup hf, lift_iSup hf']
no goals
α β : Type u
ι : Type v
ι' : Type v'
f : ι → Cardinal
f' : ι' → Cardinal
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift (f i) ≤ lift (f' (g i))
⊢ (⨆ (i : ι), lift (f i)) ≤ ⨆ (i : ι'), lift (f' i)
exact ciSup_mono' (bddAbove_range_comp.{_,_,w} hf' _) fun i => ⟨_, h i⟩