Theorems · Theorem · order theory

GaloisCoinsertion.u_iInf_l

∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → β), u (⨅ i, l (f i)) = ⨅ i, f i

Defined in

Mathlib.Order.GaloisConnection.Basic

Cited by

8 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

CompleteLatticeCompleteLattice