frestrictLe_apply

Mathlib.Order.Restriction

URI: https://scilib.ai/kg/mathlib#Preorder.frestrictLe_apply

English

Restriction on frestrictLe applied to i equals f i, for i in Iic a.

Русский

При применении frestrictLe к i, получаем то же значение f i, для i ∈ Iic a.

LaTeX

$$$\\forall {a} {\\pi} {f} {i} ,\\; frestrictLe a f i = f i$$$

Lean4

@[simp]
theorem frestrictLe_apply (a : α) (f : (a : α) → π a) (i : Iic a) : frestrictLe a f i = f i :=
  rfl

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

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

Разделы

Аффилиация

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