toSubsemigroup_injective — Mathlib

English

The map S ↦ toSubsemigroup(S) is injective: if toSubsemigroup(S) = toSubsemigroup(T) then S = T for nonunital subrings S,T of R.

Русский

Отображение S ↦ toSubsemigroup(S) инъективно: если toSubsemigroup(S) = toSubsemigroup(T), то S = T для S, T ⊆ R, несобственных подкольца без единицы.

LaTeX

$$$\forall R\,[\text{NonUnitalNonAssocRing } R],\forall S,T : \text{NonUnitalSubring } R,\ toSubsemigroup(S) = toSubsemigroup(T) \Rightarrow S = T.$$$

Lean4

theorem toSubsemigroup_injective : Function.Injective (toSubsemigroup : NonUnitalSubring R → Subsemigroup R)
  | _r, _s, h => ext (SetLike.ext_iff.mp h :)

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