support_update_subset — Mathlib

English

For DecidableEq α, support of f.update a b is a subset of insert a f.support.

Русский

При разрешимой эквивалентности α опора обновления состоит из элементов вставки a в опору исходной функции.

LaTeX

$$$\operatorname{supp}(f.update(a,b)) \subseteq \operatorname{insert}(a, \operatorname{supp}(f))$$$

Lean4

theorem support_update_subset [DecidableEq α] : support (f.update a b) ⊆ insert a f.support := by
  classical
  rw [support_update]
  split_ifs
  · exact (erase_subset _ _).trans (subset_insert _ _)
  · rfl

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