ext — Mathlib

English

StarSubsemiring objects are determined by their underlying carrier; if every element belongs to S exactly when it belongs to T, then S = T.

Русский

StarSubsemiring определяется по носителю: если для всех элементов верно x ∈ S ⇔ x ∈ T, то S = T.

LaTeX

$$$\forall S,T:\ StarSubsemiring(R)\; (\forall x:\ R, x \in S \leftrightarrow x \in T)\implies S=T$$$

Lean4

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

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