pi_eq_zero — Mathlib

English

For a family fv of affine maps indexed by i, equality pi fv = 0 is equivalent to the pointwise equalities fv i = 0 for all i.

Русский

Для семейства fv отображений, индексируемого по i, равенство pi fv = 0 эквивалентно тому, что для всех i выполняется fv(i) = 0.

LaTeX

$$pi fv = 0 \\iff ∀ i, fv i = 0$$

Lean4

theorem pi_eq_zero : pi fv = 0 ↔ ∀ i, fv i = 0 :=
  by
  simp only [AffineMap.ext_iff, funext_iff, pi_apply]
  exact forall_comm

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