Theorems · Theorem · order theory

Finset.inf_ite

∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f g : β → α}
  (p : β → Prop) [inst_2 : DecidablePred p],
  (s.inf fun i => if p i then f i else g i) = (Finset.filter p s).inf f ⊓ {i ∈ s | ¬p i}.inf g

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemilatticeInfOrderTopDecidablePred