injOn_subtype_val

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.injOn_subtype_val

English

The projection map from a subtype to the ambient type is injective on any subset of the subtype.

Русский

Проекция из подтипа в исходный тип инъективна на любом подмножестве подтипа.

LaTeX

$$$ \\operatorname{InjOn}(\\operatorname{Subtype.val}) s$$$

Lean4

theorem injOn_subtype_val {s : Set { x // p x }} : Set.InjOn Subtype.val s :=
  Subtype.coe_injective.injOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru