updateFinset_frestrictLe — Mathlib

English

Updating the finite restriction yields the same function on the restricted domain.

Русский

Обновление ограниченного домена влечёт сохранение значения на ограниченной области.

LaTeX

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

Lean4

@[simp]
theorem updateFinset_frestrictLe (a : α) (x : Π a, π a) : updateFinset x _ (frestrictLe a x) = x := by
  simp [frestrictLe]

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