F : Type ?u.52740
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.52752
κ : Type ?u.52755
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (sup s fun b => sup t (f b)) ≤ a ↔ (sup t fun c => sup s fun b => f b c) ≤ a
F : Type ?u.52740
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.52752
κ : Type ?u.52755
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β → γ → α
⊢ (sup s fun b => sup t (f b)) = sup t fun c => sup s fun b => f b c
refine' eq_of_forall_ge_iff fun a => _
F : Type ?u.52740
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.52752
κ : Type ?u.52755
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f b b_1 ≤ a) ↔ ∀ (b : γ), b ∈ t → ∀ (b_1 : β), b_1 ∈ s → f b_1 b ≤ a
F : Type ?u.52740
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.52752
κ : Type ?u.52755
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (sup s fun b => sup t (f b)) ≤ a ↔ (sup t fun c => sup s fun b => f b c) ≤ a
simp_rw [Finset.sup_le_iff]
no goals
F : Type ?u.52740
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.52752
κ : Type ?u.52755
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a✝ : α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f b b_1 ≤ a) ↔ ∀ (b : γ), b ∈ t → ∀ (b_1 : β), b_1 ∈ s → f b_1 b ≤ a
exact ⟨fun h c hc b hb => h b hb c hc, fun h b hb c hc => h c hc b hb⟩