chainsMap_id_f_map_mono — Mathlib

English

For an identity on G, if φ is epi, the entire family of f_i are epis.

Русский

Для идентичности на G, если φ эпиморфизм, вся семья f_i является эпиморфизмами.

LaTeX

$$∀ i, Epi ((chainsMap (MonoidHom.id G) φ).f i)$$

Lean4

instance chainsMap_id_f_map_mono {A B : Rep k G} (φ : A ⟶ B) [Mono φ] (i : ℕ) :
    Mono ((chainsMap (MonoidHom.id G) φ).f i) :=
  chainsMap_f_map_mono (MonoidHom.id G) φ (fun _ _ h => h) _

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