Theorems · Theorem · order theory

OrderIso.map_iSup

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  (x : ι → α), f (⨆ i, x i) = ⨆ i, f (x i)

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

25 results in Mathlib

Foundations

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

Assumes

CompleteLatticeCompleteLattice