codRestrict_apply

Mathlib.Order.InitialSeg

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

English

For any p, f, H, H2, and a, the value of codRestrict at a is the pair (f a, H a).

Русский

Для любых p, f, H, H2 и a значение codRestrict(p,f,H,H2) на a равно паре (f(a), H(a)).

LaTeX

$$$\text{codRestrict } p\ f\ H\ H_{2}\ a = \langle f(a), H(a) \rangle$$$

Lean4

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

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

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

Разделы

Аффилиация

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