isConnected_iff_transitive — Mathlib

English

A finite, nonempty G-set is connected if and only if the G-action is transitive.

Русский

Конечное непустое G-множество связано тогда и только тогда, когда действие G транзитивно.

LaTeX

$$$\\text{IsConnected}(X) \\iff \\text{MulAction.IsPretransitive } G \\; X.V$$$

Lean4

/-- A nonempty finite `G`-set is connected if and only if the `G`-action is transitive. -/
theorem isConnected_iff_transitive (X : Action FintypeCat G) [Nonempty X.V] :
    IsConnected X ↔ MulAction.IsPretransitive G X.V :=
  ⟨fun _ ↦ pretransitive_of_isConnected G X, fun _ ↦ isConnected_of_transitive G X.V⟩

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