ext — Mathlib

English

Extensionality principle: two nonunital star subalgebras are equal if they have the same membership relation.

Русский

Экстенсионализм: два неунифицированных звёздных подалгебры равны, если для всех элементов выполняется одинаковость членства.

LaTeX

$$$\\forall x,\\; x \\in S \\Leftrightarrow x \\in T \\;\Rightarrow\\; S = T$$$

Lean4

@[ext]
theorem ext {S T : NonUnitalStarSubalgebra R A} (h : ∀ x : A, x ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

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