instSetLike — Mathlib

English

Subalgebras of A are determined by their underlying sets: two subalgebras with the same carrier set are equal.

Русский

Подалгебры A определяются своими базовыми множествами: если у двух подалгебр одинаковые носители, то они равны.

LaTeX

$$$ \\forall S,T \\in \\mathrm{Subalgebra}(R,A), \\ S.\\carrier = T.\\carrier \\rightarrow S = T $$$

Lean4

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

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