frestrictLe_updateFinset

Mathlib.Order.Restriction

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

← MathLib Explorer

English

Frestricted Le with update equals the update restricted version.

Русский

С точностью до обновления frestrictLe совпадает с обновлением ограничения.

LaTeX

$$$\\text{frestrictLe}(a) (\\text{updateFinset } x (\\mathrm{Iic } a) y) = y$$$

Lean4

theorem frestrictLe_updateFinset {a : α} (x : Π a, π a) (y : Π b : Iic a, π b) :
    frestrictLe a (updateFinset x _ y) = y :=
  restrict_updateFinset ..

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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