English
From an orthogonal idempotents family e, one can form a new family by replacing a component using an Option-elimination construction, preserving orthogonality.
Русский
Из семейства ортогональных идемпотентов можно получить новое семейство, заменив компонент с помощью конструкции типа Option, сохранив ортогональность.
LaTeX
$$OrthogonalIdempotents (Option.elim · x e)$$
Lean4
theorem option (he : OrthogonalIdempotents e) [Fintype I] (x) (hx : IsIdempotentElem x) (hx₁ : x * ∑ i, e i = 0)
(hx₂ : (∑ i, e i) * x = 0) : OrthogonalIdempotents (Option.elim · x e)
where
idem i := i.rec hx he.idem
ortho i j
ne := by
classical
rcases i with - | i <;> rcases j with - | j
· cases ne rfl
·
simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, zero_mul] using
congr_arg (· * e j) hx₁
·
simpa only [Option.elim_some, Option.elim_none, ← mul_assoc, Finset.mul_sum, he.mul_eq, Finset.sum_ite_eq,
Finset.mem_univ, ↓reduceIte, mul_zero] using congr_arg (e i * ·) hx₂
· exact he.ortho (Option.some_inj.ne.mp ne)
