frestrictLe_updateFinset_of_le — Mathlib

English

Updating a finite index family respects frestrictLe₂ after restriction.

Русский

Обновление конечного множества индексов сохраняет frestrictLe₂ после ограничения.

LaTeX

$$$\\text{frestrictLe}(a) (\\text{updateFinset } x _ y) = \\text{frestrictLe}_2( hab ) y$$$

Lean4

theorem frestrictLe_updateFinset_of_le {a b : α} (hab : a ≤ b) (x : Π c, π c) (y : Π c : Iic b, π c) :
    frestrictLe a (updateFinset x _ y) = frestrictLe₂ hab y :=
  restrict_updateFinset_of_subset (Iic_subset_Iic.2 hab) ..

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