ext — Mathlib

English

Two subgroups are equal if they have the same elements.

Русский

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

LaTeX

$$$H = K \\iff \\forall x, x \\in H \\leftrightarrow x \\in K$$$

Lean4

/-- Two subgroups are equal if they have the same elements. -/
@[to_additive (attr := ext) /-- Two `AddSubgroup`s are equal if they have the same elements. -/
    ]
theorem ext {H K : Subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K :=
  SetLike.ext h

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