distribNeg — Mathlib

English

If α has a distributive negation, then Finset α also has a distributive negation (with DecidableEq α).

Русский

Если у α есть распределяемое отрицание, то и Finset α имеет распределяемое отрицание (при DecidableEq α).

LaTeX

$$$\\mathrm{HasDistribNeg}(\\mathrm{Finset}\\;\\alpha)$$$

Lean4

/-- `Finset α` has distributive negation if `α` has. -/
protected noncomputable def distribNeg [DecidableEq α] [Mul α] [HasDistribNeg α] : HasDistribNeg (Finset α) :=
  coe_injective.hasDistribNeg _ coe_neg coe_mul

Похожие утверждения