Theorems · Theorem · order theory

Finset.inf_sup_distrib_left

∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderTop α] (s : Finset ι) (f : ι → α) (a : α),
  a ⊔ s.inf f = s.inf fun i => a ⊔ f i

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

3 results in Mathlib

Foundations

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

Assumes

DistribLatticeOrderTop