English
From an orthogonal idempotent family e : I → R, one can form a new complete orthogonal idempotents structure on a type built from Option, given by an elimination map using the sum of e i.
Русский
Из семейства ортогональных идемпотентов e : I → R можно получить новую структуру полноcти ортогональных идемпотентов на типе, построенном через Option, с помощью отображения-elimination и суммы e i.
LaTeX
$$$\\forall e : I \\to R,\\; OrthogonalIdempotents e \\Rightarrow \\text{CompleteOrthogonalIdempotents}(\\text{Option.elim} \\cdot (1 - \\sum_{i} e(i)) e)$$$
Lean4
theorem option (he : OrthogonalIdempotents e) : CompleteOrthogonalIdempotents (Option.elim · (1 - ∑ i, e i) e)
where
__ :=
he.option _ he.isIdempotentElem_sum.one_sub (by simp [sub_mul, he.isIdempotentElem_sum.eq])
(by simp [mul_sub, he.isIdempotentElem_sum.eq])
complete := by
rw [Fintype.sum_option]
exact sub_add_cancel _ _
