α : Type u_1
β : Type ?u.83930
γ : Type ?u.83933
ι : Sort u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ (⨆ (i : ι), f i) ≤ a
α : Type u_1
β : Type ?u.83930
γ : Type ?u.83933
ι : Sort u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : a < ⨆ (i : ι), f i
⊢ ∃ i, a < f i
contrapose! h
no goals
α : Type u_1
β : Type ?u.83930
γ : Type ?u.83933
ι : Sort u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
a : α
h : ∀ (i : ι), f i ≤ a
⊢ (⨆ (i : ι), f i) ≤ a
exact ciSup_le' h