starMemClass — Mathlib

English

StarSubalgebra is a SetLike structure, i.e., it has a carrier set equipped with membership predicate.

Русский

StarSubalgebra образует структуру SetLike, то есть носитель состоит из множества с предикатом принадлежности.

LaTeX

$$$\\text{StarSubalgebra.setLike}: SetLike\\ (StarSubalgebra\\ R\\ A)\\ A$$$

Lean4

instance starMemClass : StarMemClass (StarSubalgebra R A) A where star_mem {s} := s.star_mem'

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