instCanonicallyOrderedMul — Mathlib

English

If β has a canonically ordered multiplication, then Germ l β also has a canonically ordered multiplication: the canonical order interacts with multiplication in germ form via pointwise evaluation.

Русский

Если β имеет канонически упорядоченное умножение, то Germ l β также имеет канонически упорядоченное умножение, порядок взаимодействует с умножением по координатам.

LaTeX

$$$\\text{CanonicallyOrderedMul}(\\mathrm{Germ}_l \\beta)$$$

Lean4

@[to_additive]
instance instCanonicallyOrderedMul [Mul β] [LE β] [CanonicallyOrderedMul β] : CanonicallyOrderedMul (Germ l β)
    where
  le_mul_self x y := inductionOn₂ x y fun _ _ ↦ Eventually.of_forall fun _ ↦ le_mul_self
  le_self_mul x y := inductionOn₂ x y fun _ _ ↦ Eventually.of_forall fun _ ↦ le_self_mul

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