has_non_trivial_subobject_of_not_isConnected_of_not_initial

English

An object that is not initial or connected has a nontrivial subobject.

Русский

Объект, не являющийся начальным или связным, имеет неверный подобъект.

LaTeX

$$$\\forall X\\,\\neg\\mathrm{IsConnected}(X) \\Rightarrow \\exists Y\\,\\exists v:\\,Y\\to X\\;\\bigl(\\mathrm{IsInitial}(Y) \\Rightarrow \\mathrm{False}\\bigr) \\land \\mathrm{Mono}(v) \\land \\lnot \\mathrm{IsIso}(v)$$$

Lean4

/-- An object that is neither initial or connected has a non-trivial subobject. -/
theorem has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬IsConnected X)
    (hi : IsInitial X → False) : ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬IsIso v) :=
  by
  contrapose! hc
  exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩

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