topologicalClosure_coe — Mathlib

English

The carrier of the topological closure of a nonunital subsemiring coincides with the closure of its carriers.

Русский

Область топологического замыкания подпол semiring совпадает с замыканием его носителя.

LaTeX

$$$\\big( s.topologicalClosure : Set R \\big) = \\overline{\,s\}$$$

Lean4

@[simp]
theorem topologicalClosure_coe (s : NonUnitalSubsemiring R) :
    (s.topologicalClosure : Set R) = _root_.closure (s : Set R) :=
  rfl

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