Theorems · Theorem · order theory

GaloisConnection.l_ciSup

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {f : ι → α}, BddAbove (Set.range f) → l (⨆ i, f i) = ⨆ i, l (f i)

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Indexed

Cited by

3 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLatticeConditionallyCompleteLatticeNonempty