theorem
ciSup₂_le'
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[ConditionallyCompleteLinearOrderBot α]
{a : α}
{f : (i : ι) → κ i → α}
(h : ∀ (i : ι) (j : κ i), f i j ≤ a)
:
theorem
exists_lt_of_lt_ciSup₂'
{α : Type u_1}
{ι : Sort u_2}
{κ : ι → Sort u_3}
[ConditionallyCompleteLinearOrderBot α]
{a : α}
{f : (i : ι) → κ i → α}
(h : a < ⨆ (i : ι), ⨆ (j : κ i), f i j)
:
∃ (i : ι) (j : κ i), a < f i j