theorem ciSup_le_ciSup {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [ConditionallyCompleteLattice α] {f : ι → α} {g : ι' → α} (h₀ : ∀ (i : ι), ∃ (j : ι'), f i ≤ g j) (hg : BddAbove (Set.range g)) : ⨆ (i : ι), f i ≤ ⨆ (j : ι'), g j

theorem ciSup_eq_ciSup {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [ConditionallyCompleteLinearOrder α] {f : ι → α} {g : ι' → α} (h₀ : ∀ (i : ι), ∃ (j : ι'), f i ≤ g j) (h₁ : ∀ (j : ι'), ∃ (i : ι), g j ≤ f i) : ⨆ (i : ι), f i = ⨆ (j : ι'), g j