codRestrict_apply

Mathlib.Logic.Embedding.Set

URI: https://scilib.ai/kg/mathlib#Function.Embedding.codRestrict_apply

English

The value of codRestrict p f H on a is precisely (f a, H a).

Русский

Значение codRestrict p f H на элементе a равно (f a, H a).

LaTeX

$$$\\text{codRestrict } p\\; f\\; H\\; a = \\langle f a, H a\\rangle$$$

Lean4

@[simp]
theorem codRestrict_apply {α β} (p) (f : α ↪ β) (H a) : codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

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

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

Разделы

Аффилиация

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