codRestrict_apply

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.codRestrict_apply

English

For any a, (codRestrict p f H) a equals the pair ⟨f a, H a⟩.

Русский

Для любого a отображение codRestrict p f H(a) равно паре ⟨f(a), H(a)⟩.

LaTeX

$$$codRestrict(p)(f)(H)(a) = \\langle f(a), H(a) \\rangle.$$$

Lean4

@[simp]
theorem codRestrict_apply (p) (f : r ≼i s) (H a) : codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

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

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

Разделы

Аффилиация

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