Theorems · Theorem · order theory

Set.map_finite_biInf

∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [InfTopHomClass F α β] {s : Set ι},
  s.Finite → ∀ (f : F) (g : ι → α), f (⨅ x ∈ s, g x) = ⨅ x ∈ s, f (g x)

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLatticeCompleteLatticeFunLikeInfTopHomClass