Theorems · Theorem · order theory

sSup_image2_eq_sSup_sSup

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) → sSup (Set.image2 l s t) = l (sSup s) (sSup t)

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

5 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLatticeCompleteLatticeCompleteLattice