Theorems · Theorem · order theory

Finset.sup_inf_distrib_right

∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α) (a : α),
  s.sup f ⊓ a = s.sup 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

DistribLatticeOrderBot