instSetLike — Mathlib

English

There is a SetLike instance for Ideals identifying the carrier with the underlying set.

Русский

Существует экземпляр SetLike для Ideals, который связывает носитель с подлежащим множеством.

LaTeX

$$$ \\text{SetLike}(\\text{Ideal } P)\\; P\\text{ with } (s \\mapsto s.\\text{carrier}) $$$

Lean4

instance : SetLike (Ideal P) P where
  coe s := s.carrier
  coe_injective' _ _ h := toLowerSet_injective <| SetLike.coe_injective h

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