case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)
rintro _ ⟨a, b, ha, hb, rfl⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
a✝ : α
b✝ : β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
b : β
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds t
⊢ f a b ∈ upperBounds (image2 f s t)
exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb