English
If p and q are idempotent endomorphisms of a vector space, then p = q if and only if both their images and their kernels coincide.
Русский
Если p и q — идемпотентные эндоморфизмы на векторном пространстве, то p = q тогда и только тогда, когда совпадают их образы и ядра.
LaTeX
$$$ p = q \iff \operatorname{Im}(p) = \operatorname{Im}(q) \land \ker(p) = \ker(q) $$$
Lean4
/-- Idempotent operators are equal iff their range and kernels are. -/
theorem ext_iff {p q : E →ₗ[R] E} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
p = q ↔ range p = range q ∧ ker p = ker q :=
by
refine ⟨fun h => ⟨congrArg range h, congrArg ker h⟩, fun ⟨hr, hk⟩ => ?_⟩
ext x
obtain ⟨⟨v, hv⟩, ⟨w, hw⟩, rfl, _⟩ := (ker p).existsUnique_add_of_isCompl hp.isCompl.symm x
simp [mem_ker.mp, hv, (hk ▸ hv), (mem_range_iff hp).mp, hw, (mem_range_iff hq).mp, (hr ▸ hw)]
