ext — Mathlib

English

Two von Neumann algebras on H are equal if and only if they contain exactly the same elements.

Русский

Две алгебры Вона на H равны тогда и только тогда, когда содержат одни и те же элементы.

LaTeX

$$$\\forall S,T: \\text{VonNeumannAlgebra } H,\\; (\\forall x, x\\in S \\iff x\\in T) \\Rightarrow S = T.$$$

Lean4

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

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