val_codRestrict_apply

Mathlib.Data.Set.Restrict

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

English

The evaluation of the codomain-restricted function on x is just f x, i.e., the value in α is preserved when viewing through the restriction.

Русский

Значение codRestrict на x равняется f x; проекция сохраняется.

LaTeX

$$$(codRestrict f s h\\; x : s) = f x$$$

Lean4

@[simp]
theorem val_codRestrict_apply (f : ι → α) (s : Set α) (h : ∀ x, f x ∈ s) (x : ι) : (codRestrict f s h x : α) = f x :=
  rfl

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

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

Разделы

Аффилиация

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