Theorems · Theorem · order theory

Set.map_finite_iSup

∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [SupBotHomClass F α β] [Finite ι] (f : F) (g : ι → α), f (⨆ i, g i) = ⨆ i, f (g i)

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLatticeCompleteLatticeFunLikeSupBotHomClassFinite