map — Mathlib

English

If e is a complete orthogonal idempotents family, then f ∘ e is also complete and orthogonal idempotents.

Русский

Если e образует полную ортогональную систему идемпотентов, то f ∘ e также образует полную ортогональную систему идемпотентов.

LaTeX

$$CompleteOrthogonalIdempotents.map f e$$

Lean4

theorem map (he : CompleteOrthogonalIdempotents e) : CompleteOrthogonalIdempotents (f ∘ e)
    where
  __ := he.toOrthogonalIdempotents.map f
  complete := by simp only [Function.comp_apply, ← map_sum, he.complete, map_one]

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