instSemiring — Mathlib

English

If R is a semiring with bounded and continuous multiplication and additions, then α →ᵇ R is a semiring with pointwise addition and multiplication.

Русский

Если R — полукольцо с ограниченным и непрерывным умножением и сложением, то α →ᵇ R образует полукольцо с покоординатным сложением и умножением.

LaTeX

$$$\text{instSemiring }(\alpha \to^{\mathrm{b}} R)$$$

Lean4

instance instSemiring {R : Type*} [TopologicalSpace α] [PseudoMetricSpace R] [Semiring R] [BoundedMul R]
    [ContinuousMul R] [BoundedAdd R] [ContinuousAdd R] : Semiring (α →ᵇ R) :=
  Injective.semiring _ DFunLike.coe_injective' rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ ↦ rfl)

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