simple_iff_subobject_isSimpleOrder

English

A object X is simple if and only if Subobject X is a simple order.

Русский

Объект X прост тогда и только тогда, когда Subobject X — простой порядок.

LaTeX

$$$ Simple\ X \iff IsSimpleOrder(Subobject\ X). $$$

Lean4

/-- `X` is simple iff it has subobject lattice `{⊥, ⊤}`. -/
theorem simple_iff_subobject_isSimpleOrder (X : C) : Simple X ↔ IsSimpleOrder (Subobject X) :=
  ⟨by
    intro h
    infer_instance, by
    intro h
    exact simple_of_isSimpleOrder_subobject X⟩

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