mk_surjective — Mathlib

English

Every subobject S of X is representable as mk i for some object A and mono i: A → X.

Русский

Каждое подмножество S ⊆ X представимо как mk i для некоторого A и моно i: A → X.

LaTeX

$$$\\exists A\\,\\exists i:\\, A \\to X\\;([Mono\\ i])\\; S = Subobject.mk i$$$

Lean4

theorem mk_surjective {X : C} (S : Subobject X) : ∃ (A : C) (i : A ⟶ X) (_ : Mono i), S = Subobject.mk i :=
  ⟨_, S.arrow, inferInstance, by simp⟩
    -- We make `X` and `Y` explicit arguments here so that when `ofLE` appears in goal statements
    -- it is possible to see its source and target
    -- (`h` will just display as `_`, because it is in `Prop`).

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