Theorems · Theorem · order theory

GaloisConnection.u_inf

∀ {β : Type u} {α : Type v} {b₁ b₂ : β} [inst : SemilatticeInf β] [inst_1 : SemilatticeInf α] {u : β → α} {l : α → β},
  GaloisConnection l u → u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

37 results in Mathlib

Foundations

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

Assumes

SemilatticeInfSemilatticeInf