Theorems · Theorem · order theory

csInf_image2_eq_csInf_csInf

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

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLatticeConditionallyCompleteLattice