Agreement of functions away from a finite set

Two functions f and g agree away from a finset S when ∀ x ∉ S, f x = g x. This file records how such an agreement condition changes when a point is added to S, and when one of the functions is updated at a point inside or outside S. These are the steps that move an updated coordinate in and out of a comparison of tuples, as in the matrix entries of operators acting on finitely many coordinates of a tuple.

Main results

• Finset.forall_notMem_iff_forall_notMem_insert: a property holds away from s iff it holds away from insert a s and at a, for a ∉ s.
• Function.forall_notMem_update_eq_iff_of_mem: updating f at a point of S does not change where it agrees with g away from S.
• Function.forall_notMem_update_eq_iff_of_notMem: updating f at a point a ∉ S to b agrees with g away from S iff f agrees with g away from insert a S and b = g a.

theorem Finset.forall_notMem_iff_forall_notMem_insert {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {p : α → Prop} (h : a ∉ s) : (∀ x ∉ s, p x) ↔ (∀ x ∉ insert a s, p x) ∧ p a

A property holds away from s iff it holds away from insert a s and at a, for a ∉ s.

@[simp]

theorem Function.forall_notMem_update_eq_iff_of_mem {α : Type u_1} [DecidableEq α] {β : α → Type u_2} {S : Finset α} {a : α} {f g : (x : α) → β x} {b : β a} (h : a ∈ S) : (∀ x ∉ S, update f a b x = g x) ↔ ∀ x ∉ S, f x = g x

Updating f at a point of S does not change where it agrees with g away from S.

@[simp]

theorem Function.forall_notMem_update_eq_iff_of_notMem {α : Type u_1} [DecidableEq α] {β : α → Type u_2} {S : Finset α} {a : α} {f g : (x : α) → β x} {b : β a} (h : a ∉ S) : (∀ x ∉ S, update f a b x = g x) ↔ (∀ x ∉ insert a S, f x = g x) ∧ b = g a

Updating f at a point a ∉ S to b agrees with g away from S iff f agrees with g away from insert a S and b = g a.