ext — Mathlib

English

Two submonoids are equal if they have the same elements.

Русский

Два подмономиода равны, если и только если у них одинаковые элементы.

LaTeX

$$$$ S = T \\iff (\\forall x, x \\in S \\leftrightarrow x \\in T) $$$$

Lean4

/-- Two submonoids are equal if they have the same elements. -/
@[to_additive (attr := ext) /-- Two `AddSubmonoid`s are equal if they have the same elements. -/
    ]
theorem ext {S T : Submonoid M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

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