instSubtypeSet — Mathlib

English

There is a SetLike structure on the subtype {s ∈ X | p s} with coe equal to the inclusion and coe_injective given by Subtype.val_injective.

Русский

Существует структура SetLike на подтипе {s ∈ X | p s}, где отображение к X есть включение, а инъективность коэрции задаётся Subtype.val_injective.

LaTeX

$$$ \mathrm{instSubtypeSet} : \SetLike{ s \;\/\/\; p\ s } X \\ \\ \text{coe} := (\\uparrow) \\ \text{coe_injective'} := \text{Subtype.val_injective}$$$

Lean4

/-- membership is inherited from `Set X` -/
abbrev instSubtypeSet {X} {p : Set X → Prop} : SetLike { s // p s } X
    where
  coe := (↑)
  coe_injective' := Subtype.val_injective

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