α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.111757
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
c : γ
⊢ sSup (image2 l s t) ≤ c ↔ l (sSup s) (sSup t) ≤ c
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.111757
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)
refine' eq_of_forall_ge_iff fun c => _
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.111757
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
c : γ
⊢ (∀ (i₂ : β), i₂ ∈ t → ∀ (i₁ : α), i₁ ∈ s → l i₁ i₂ ≤ c) ↔ ∀ (b : β), b ∈ t → b ≤ u₂ (sSup s) c
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.111757
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
c : γ
⊢ sSup (image2 l s t) ≤ c ↔ l (sSup s) (sSup t) ≤ c
rw [csSup_le_iff (hs₁.image2 (fun _ => (h₁ _).monotone_l) (fun _ => (h₂ _).monotone_l) ht₁)
    (hs₀.image2 ht₀),
  forall_image2_iff, forall₂_swap, (h₂ _).le_iff_le, csSup_le_iff ht₁ ht₀]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Sort ?u.111757
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : α → β → γ
s : Set α
t : Set β
l u : α → β → γ
l₁ u₁ : β → γ → α
l₂ u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : Set.Nonempty s
hs₁ : BddAbove s
ht₀ : Set.Nonempty t
ht₁ : BddAbove t
c : γ
⊢ (∀ (i₂ : β), i₂ ∈ t → ∀ (i₁ : α), i₁ ∈ s → l i₁ i₂ ≤ c) ↔ ∀ (b : β), b ∈ t → b ≤ u₂ (sSup s) c
simp_rw [← (h₂ _).le_iff_le, (h₁ _).le_iff_le, csSup_le_iff hs₁ hs₀]