Theorems · Theorem · order theory

Finset.sup_inf_sup

∀ {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι)
  (t : Finset κ) (f : ι → α) (g : κ → α), s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2

Defined in

Mathlib.Data.Finset.Lattice.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

DistribLatticeOrderBot