instDistribNeg — Mathlib

English

If α has a multiplication and a distributive negation, then Filter α inherits a distributive negation.

Русский

Если у α есть умножение и распределительное отрицание, то Filter α наследует распределительное отрицание.

LaTeX

$$[Mul α] [HasDistribNeg α] ⇒ HasDistribNeg(\\mathrm{Filter}(α))$$

Lean4

/-- `Filter α` has distributive negation if `α` has. -/
protected def instDistribNeg [Mul α] [HasDistribNeg α] : HasDistribNeg (Filter α) :=
  { Filter.instInvolutiveNeg with
    neg_mul := fun _ _ => map₂_map_left_comm neg_mul
    mul_neg := fun _ _ => map_map₂_right_comm mul_neg }

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