restrict_eq

Mathlib.Data.Set.Restrict

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

English

The restriction of the identity to a set s is the inclusion map from s into α.

Русский

Ограничение тождественного к множеству s есть включение из s в α.

LaTeX

$$$\operatorname{restrict}(s, \mathrm{id}) = \operatorname{Subtype.val}$$$

Lean4

theorem restrict_eq (f : α → β) (s : Set α) : s.restrict f = f ∘ Subtype.val :=
  rfl

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

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

Разделы

Аффилиация

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