coe_toSubsemiring — Mathlib

English

The underlying set of a StarSubsemiring S is exactly the carrier of its toSubsemiring, i.e., the embedding is faithful on carriers.

Русский

Подмножество StarSubsemiring S эквивалентно носителю его toSubsemiring, тождество элементов сохраняется на носителе.

LaTeX

$$$ (S.toSubsemiring : Set R) = S $$$

Lean4

@[simp]
theorem coe_toSubsemiring (S : StarSubsemiring R) : (S.toSubsemiring : Set R) = S :=
  rfl

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