Universal statements split at two points

A statement holds everywhere exactly when it holds at two given points and at every point different from both. This is the form in which agreement of two functions is checked when two distinguished coordinates are treated separately from the rest.

Main results

• TauCeti.forall_iff_forall_ne_ne_and: ∀ i, P i iff P holds away from p and q, at p, and at q.

theorem TauCeti.forall_iff_forall_ne_ne_and {α : Sort u_1} {P : α → Prop} (p q : α) : (∀ (i : α), P i) ↔ (∀ (i : α), i ≠ p → i ≠ q → P i) ∧ P p ∧ P q

A statement holds everywhere exactly when it holds at two given points and away from them.