case inl
α : Type u_1
β : Type ?u.55772
γ : Type ?u.55775
ι : Sort u_2
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a b : α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g

case inr
α : Type u_1
β : Type ?u.55772
γ : Type ?u.55775
ι : Sort u_2
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a b : α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
α : Type u_1
β : Type ?u.55772
γ : Type ?u.55775
ι : Sort u_2
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a b : α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g
cases isEmpty_or_nonempty ι
no goals
case inl
α : Type u_1
β : Type ?u.55772
γ : Type ?u.55775
ι : Sort u_2
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a b : α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : IsEmpty ι
⊢ iSup f ≤ iSup g
rw [iSup_of_empty', iSup_of_empty']
no goals
case inr
α : Type u_1
β : Type ?u.55772
γ : Type ?u.55775
ι : Sort u_2
inst✝ : ConditionallyCompleteLattice α
s t : Set α
a b : α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h✝ : Nonempty ι
⊢ iSup f ≤ iSup g
exact ciSup_le fun x => le_ciSup_of_le B x (H x)