pretransitive_iff_unique_quotient_of_nonempty

English

If α is nonempty, a pretransitive action is equivalent to the quotient having a unique element.

Русский

Если α непусто, пре-транситивность эквивалентна тому, что квотиент имеет единственный элемент.

LaTeX

$$IsPretransitive G α \iff Nonempty (Unique (orbitRel.Quotient G α))$$

Lean4

/-- If `α` is non-empty, an action is pretransitive if and only if the quotient has exactly one
element. -/
@[to_additive /-- If `α` is non-empty, an additive action is pretransitive if and only if the
    quotient has exactly one element. -/
    ]
theorem pretransitive_iff_unique_quotient_of_nonempty [Nonempty α] :
    IsPretransitive G α ↔ Nonempty (Unique <| orbitRel.Quotient G α) :=
  by
  rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

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