piFinset_update_singleton_eq_filter_piFinset_eq

English

If the i-th coordinate is updated to a singleton {a} and a ∈ s i, then piFinset(update s i {a}) equals the set of those f in piFinset s with f(i)=a.

Русский

Если i-я координата обновлена до единственного элемента {a} и a ∈ s i, то piFinset(update s i {a}) равен множеству функций f ∈ piFinset s с условием f(i)=a.

LaTeX

$$$\\operatorname{piFinset}(\\operatorname{update} s i {a}) = \\{ f \\in \\operatorname{piFinset}(s) \\mid f(i) = a \\}$, при условии $a \\in s(i)$.$$

Lean4

theorem piFinset_update_singleton_eq_filter_piFinset_eq (s : ∀ i, Finset (δ i)) (i : α) {a : δ i} (ha : a ∈ s i) :
    piFinset (Function.update s i { a }) = {f ∈ piFinset s | f i = a} := by
  simp [piFinset_update_eq_filter_piFinset_mem, ha]

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