map_injective_iff — Mathlib

English

If f is injective, then CompleteOrthogonalIdempotents (f ∘ e) ↔ CompleteOrthogonalIdempotents e.

Русский

Если f инъективен, то CompleteOrthogonalIdempotents (f ∘ e) эквивалентно CompleteOrthogonalIdempotents e.

LaTeX

$$CompleteOrthogonalIdempotents (f ∘ e) ↔ CompleteOrthogonalIdempotents e$$

Lean4

theorem map_injective_iff (hf : Function.Injective f) :
    CompleteOrthogonalIdempotents (f ∘ e) ↔ CompleteOrthogonalIdempotents e := by
  simp [completeOrthogonalIdempotents_iff, ← hf.eq_iff, OrthogonalIdempotents.map_injective_iff f hf]

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