Theorems · Theorem · order theory

isLUB_image2_of_isLUB_isLUB

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

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

PreorderPreorderPreorder