instContinuousNegMulOpposite — Mathlib

English

If R is a nonunital nonassociative semiring, and R is a topological semiring, then MulOpposite R is a topological semiring.

Русский

Если R — полукольцо без единицы и R — топологическое полукольцо, то MulOpposite R тоже топологическое полукольцо.

LaTeX

$$IsTopologicalSemiring (MulOpposite R)$$

Lean4

instance [NonUnitalNonAssocRing R] [TopologicalSpace R] [ContinuousNeg R] : ContinuousNeg Rᵐᵒᵖ :=
  opHomeomorph.symm.isInducing.continuousNeg fun _ => rfl

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