topologicalSemiring — Mathlib

English

With discrete topology, a nonunital semiring is automatically a topological semiring.

Русский

При дискретной топологии неограниченное полукольцо автоматически становится топологическим полукольцом.

LaTeX

$$$\\mathrm{IsTopologicalSemiring}(\\text{DiscreteTopology}(R))$$$

Lean4

instance (priority := 50) topologicalSemiring [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [DiscreteTopology R] :
    IsTopologicalSemiring R :=
  ⟨⟩

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