Theorems · Theorem · order theory

Finset.inf_comm

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β)
  (t : Finset γ) (f : β → γ → α), (s.inf fun b => t.inf (f b)) = t.inf fun c => s.inf fun b => f b c

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemilatticeInfOrderTop