mk₁_surjective — Mathlib

English

Every object in ComposableArrows C 1 arises as mk₁ f for some morphism f: X0 ⟶ X1.

Русский

Каждый объект в ComposableArrows C 1 получается как mk₁ f для некоторого морфизма f: X0 ⟶ X1.

LaTeX

$$$\forall X : ComposableArrows\ C\ 1, \exists X_0 X_1\ (f: X_0 ⟶ X_1), X = mk_1 f$$$

Lean4

theorem mk₁_surjective (X : ComposableArrows C 1) : ∃ (X₀ X₁ : C) (f : X₀ ⟶ X₁), X = mk₁ f :=
  ⟨_, _, X.map' 0 1, ext₁ rfl rfl (by simp)⟩

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