isomorphisms_le_pushouts_generatingMonomorphisms

English

The set of isomorphisms is less than or equal to the pushouts generated by G.

Русский

Множество изоморфизмов содержится в границах pushouts, порождаемых G.

LaTeX

$$$\text{isomorphisms } C \leq (generatingMonomorphisms G).pushouts$$$

Lean4

theorem isomorphisms_le_pushouts_generatingMonomorphisms [HasZeroMorphisms C] :
    MorphismProperty.isomorphisms C ≤ (generatingMonomorphisms G).pushouts :=
  MorphismProperty.isomorphisms_le_pushouts _ (fun _ ↦ ⟨_, _, _, ⟨⊤⟩, 0, inferInstance⟩)

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