ext — Mathlib

English

Two subsemigroups are equal if and only if they have the same elements.

Русский

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

LaTeX

$$$ \forall S,T : Subsemigroup M, \ (\\forall x, x \\in S \\iff x \\in T) \\Rightarrow S = T $$$

Lean4

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

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