mk — Mathlib · SciLib

English

There exists strong epi-mono factorisations for every morphism: for all X,Y and f: X ⟶ Y, there exists I, e: X ⟶ I, m: I ⟶ Y with f = m ∘ e and e strong epi, m mono.

Русский

Существуют сильные эпиморфно-монодные факторизации для каждого отображения: для любых X,Y и f: X ⟶ Y существует I, e: X ⟶ I, m: I ⟶ Y с f = m ∘ e и e — сильная эпиморфия, m — моно.

LaTeX

$$$\forall X,Y,f: X \to Y, \exists I, e: X \to I, m: I \to Y, f = m \circ e \wedge (StrongEpi\,e) \wedge (Mono\,m)$$$

Lean4

theorem mk (d : ∀ {X Y : C} (f : X ⟶ Y), StrongEpiMonoFactorisation f) : HasStrongEpiMonoFactorisations C :=
  ⟨fun f => Nonempty.intro <| d f⟩

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