Theorems · Theorem · order theory

Function.update_inf

∀ {ι : Type u_1} {π : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i)
  (i : ι) (a b : π i), Function.update f i (a ⊓ b) = Function.update f i a ⊓ Function.update f i b

Defined in

Mathlib.Order.Lattice

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqSemilatticeInf