le_minOrder — Mathlib

English

For any n in ENat, n ≤ minOrder α if and only if for every a ≠ 1 with IsOfFinOrder a we have n ≤ order(a).

Русский

Для любой n ∈ ENat верно: n ≤ minOrder α тогда и только тогда, когда для каждого a ≠ 1 с IsOfFinOrder(a) имеем n ≤ order(a).

LaTeX

$$$n \le \minOrder(\alpha) \iff \forall a\ (a \neq 1 \land IsOfFinOrder(a) \Rightarrow n \le \operatorname{order}(a))$$$

Lean4

@[to_additive (attr := simp)]
theorem le_minOrder {n : ℕ∞} : n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ orderOf a := by simp [minOrder]

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