Theorems · Theorem · order theory

Finset.inf_sup_distrib_right

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

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

2 results in Mathlib

Foundations

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

Assumes

DistribLatticeOrderTop