instSetLike — Mathlib

English

The collection of nonunital star subalgebras carries a SetLike structure, with carrier given by the underlying set and a provenance for coercion.

Русский

Множество нон-юнит Star-подалгебр имеет структуру SetLike, носитель которой — соответствующее подмножество, с заданной связью коэрции.

LaTeX

$$$\\text{SetLike} (\\text{NonUnitalStarSubalgebra } R A) A$$$

Lean4

instance instSetLike : SetLike (NonUnitalStarSubalgebra R A) A
    where
  coe {s} := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective h

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