subtractionCommMonoid — Mathlib

English

The collection of intervals on α carries a natural SubtractionCommMonoid structure inherited from the additive structure of α; neg, sub are defined by negation and subtraction in α, and the axioms hold accordingly.

Русский

Множество интервалов над α естественно образует SubtractionCommMonoid, наследуя операции вычитания из операции сложения в α; отрицание и вычитание задаются через соответствующие операции α, и выполняются соответствующие аксиомы.

LaTeX

$$$ \text{SubtractionCommMonoid}(\text{Interval}(\alpha)) $$$

Lean4

instance subtractionCommMonoid {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :
    SubtractionCommMonoid (NonemptyInterval α) :=
  { NonemptyInterval.addCommMonoid with
    neg := Neg.neg
    sub := Sub.sub
    sub_eq_add_neg := fun s t => by refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;> exact sub_eq_add_neg _ _
    neg_neg := fun s => by apply NonemptyInterval.ext; exact neg_neg _
    neg_add_rev := fun s t => by refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;> exact neg_add_rev _ _
    neg_eq_of_add := fun s t h =>
      by
      obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
      rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
        -- TODO: use a better defeq

    zsmul := zsmulRec }

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