Theorems · Theorem · order theory

csSup_image2_eq_csSup_csSup

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
  {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
    (∀ (a : α), GaloisConnection (l a) (u₂ a)) →
      s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sSup s) (sSup t)

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLatticeConditionallyCompleteLattice