isOfFinOrder_iff — Mathlib

English

If f is injective, IsOfFinOrder is preserved in both directions between x and f(x).

Русский

Если f инъективен, то свойство конечного порядка сохраняется между x и f(x) в обе стороны.

LaTeX

$$$ \forall {G H} [Monoid G][Monoid H] {f : G \to_* H} (hf : Injective f) : IsOfFinOrder x \leftrightarrow IsOfFinOrder (f(x))$$$

Lean4

@[to_additive]
theorem isOfFinOrder_iff [Monoid H] {f : G →* H} (hf : Injective f) : IsOfFinOrder (f x) ↔ IsOfFinOrder x := by
  rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]

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