Theorems · Theorem · order theory

isGLB_image2_of_isGLB_isGLB

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

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

PreorderPreorderPreorder