period_bounded_of_exponent_pos — Mathlib

English

For exp_pos: 0 < exponent(M), the set {period(m,a) : a ∈ α} is bounded above by exponent(M).

Русский

При 0 < экспонента(M) множество {period(m,a) : a ∈ α} ограничено сверху экспонентой M.

LaTeX

$$0 < \operatorname{exponent}(M) \Rightarrow \forall a \in \alpha, \ \operatorname{period}(m,a) \le \operatorname{exponent}(M).$$

Lean4

@[to_additive]
theorem period_bounded_of_exponent_pos (exp_pos : 0 < Monoid.exponent M) (m : M) :
    BddAbove (Set.range (fun a : α => period m a)) :=
  by
  use Monoid.exponent M
  simpa [upperBounds] using period_le_exponent exp_pos _

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