α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
t : Cardinal
⊢ (⨆ (i : ι), lift (f i)) ≤ t ↔ ∀ (i : ι), lift (f i) ≤ t
α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
t : Cardinal
⊢ lift (iSup f) ≤ t ↔ ∀ (i : ι), lift (f i) ≤ t
rw [lift_iSup hf]
no goals
α β : Type u
ι : Type v
f : ι → Cardinal
hf : BddAbove (range f)
t : Cardinal
⊢ (⨆ (i : ι), lift (f i)) ≤ t ↔ ∀ (i : ι), lift (f i) ≤ t
exact ciSup_le_iff' (bddAbove_range_comp.{_,_,u} hf _)