of_prod_one_sub — Mathlib

English

If e is a complete orthogonal idempotent system and the product of (1 - e_i) equals 0, then e is a complete system.

Русский

Если e является полной ортогональной системой идемпотентов и произведение (1 − e_i) равно 0, тогда e образует полную систему.

LaTeX

$$$(he : CompleteOrthogonalIdempotents e) \\Rightarrow ((\\prod i, (1 - e i)) = 0) \\Rightarrow CompleteOrthogonalIdempotents e$$$

Lean4

theorem of_prod_one_sub (he : OrthogonalIdempotents e) (he' : ∏ i, (1 - e i) = 0) : CompleteOrthogonalIdempotents e
    where
  __ := he
  complete := by rwa [he.prod_one_sub, sub_eq_zero, eq_comm] at he'

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