mk_surjective — Mathlib

English

For any m in M F, there exist j ∈ J and x ∈ F.obj j such that M.mk F ⟨j,x⟩ = m; i.e., surjectivity of the quotient construction to ColimitType.

Русский

Для любого элемента m в M F существует j ∈ J и x ∈ F.obj j так, что M.mk F ⟨j,x⟩ = m.

LaTeX

$$$\exists j:\, J,\; \exists x:\, F.obj j,\; M.mk F ⟨j,x⟩ = m.$$$

Lean4

@[to_additive]
theorem mk_surjective (m : M.{v, u} F) : ∃ (j : J) (x : F.obj j), M.mk F ⟨j, x⟩ = m :=
  (F ⋙ forget MonCat).ιColimitType_jointly_surjective m

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