α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) ≤ ⨆ (i : ι), f i ⊓ g i
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ (i : ι), f i ⊓ g i) = (⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i
refine' (le_iSup_inf_iSup f g).antisymm _
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ (i : ι × ι), f i.fst ⊓ g i.snd) ≤ ⨆ (i : ι), f i ⊓ g i
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) ≤ ⨆ (i : ι), f i ⊓ g i
rw [iSup_inf_iSup]
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
⊢ ∃ i', f i.fst ⊓ g i.snd ≤ f i' ⊓ g i'
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ (i : ι × ι), f i.fst ⊓ g i.snd) ≤ ⨆ (i : ι), f i ⊓ g i
refine' iSup_mono' fun i => _
no goals
case intro.intro
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.12298
inst✝² : Frame α
s t : Set α
a b : α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x x_1 => x ≤ x_1
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.fst ≤ j
h₂ : i.snd ≤ j
⊢ ∃ i', f i.fst ⊓ g i.snd ≤ f i' ⊓ g i'
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩