α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.5320
inst✝ : Frame α
s✝ t✝ : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ (i : { i // i ∈ s } × { i // i ∈ t }), f ↑i.fst ⊓ g ↑i.snd) = ⨆ (x : { i // i ∈ s ×ˢ t }), f (↑x).fst ⊓ g (↑x).snd
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.5320
inst✝ : Frame α
s✝ t✝ : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ ((⨆ (i : ι) (_ : i ∈ s), f i) ⊓ ⨆ (j : ι') (_ : j ∈ t), g j) = ⨆ (p : ι × ι') (_ : p ∈ s ×ˢ t), f p.fst ⊓ g p.snd
simp only [iSup_subtype', iSup_inf_iSup]
no goals
α : Type u
β : Type v
ι✝ : Sort w
κ : ι✝ → Sort ?u.5320
inst✝ : Frame α
s✝ t✝ : Set α
a b : α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ (⨆ (i : { i // i ∈ s } × { i // i ∈ t }), f ↑i.fst ⊓ g ↑i.snd) = ⨆ (x : { i // i ∈ s ×ˢ t }), f (↑x).fst ⊓ g (↑x).snd
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl