case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ BddAbove (s ∪ t)
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)
rintro ⟨bs, hs⟩ ⟨bt, ht⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds (s ∪ t)
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ BddAbove (s ∪ t)
use bs ⊔ bt
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds s ∩ upperBounds t
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds (s ∪ t)
rw [upperBounds_union]
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t✝ : Set α
a b : α
inst✝ : SemilatticeSup γ
s t : Set γ
bs : γ
hs : bs ∈ upperBounds s
bt : γ
ht : bt ∈ upperBounds t
⊢ bs ⊔ bt ∈ upperBounds s ∩ upperBounds t
exact ⟨upperBounds_mono_mem le_sup_left hs, upperBounds_mono_mem le_sup_right ht⟩