instIsConnectedOfIsPretransitiveOfNonempty

English

If the action of M on X is pretransitive and X is nonempty, then the action category is connected (any two objects can be joined by a zigzag of morphisms).

Русский

Если действие M на X предварительно транситивно и X непусто, то категория действий связна: любые два объекта можно соединить зигзагообразной цепью морфизмов.

LaTeX

$$$[IsPretransitive\ M\ X] \; [Nonempty\ X] \Rightarrow \mathrm{IsConnected}(\mathsf{ActionCategory}(M,X))$$$

Lean4

instance [IsPretransitive M X] [Nonempty X] : IsConnected (ActionCategory M X) :=
  zigzag_isConnected fun x y =>
    Relation.ReflTransGen.single <| Or.inl <| nonempty_subtype.mpr (show _ from exists_smul_eq M x.back y.back)

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