English
Equivalently, n ≤ minOrder G if and only if for every subgroup s of G with s ≠ ⊥ and finite, n ≤ card(s).
Русский
Эквивалентно, n ≤ minOrder G тогда и только тогда, когда для каждой подгруппы s ⊆ G с s ≠ ⊥ и конечной мощностью выполнено n ≤.card(s).
LaTeX
$$$n \le \minOrder(G) \iff \forall s \le G, s \neq \{1\}, \ (s, \mathbb{R})\text{ finite} \Rightarrow n \le |s|$$$
Lean4
@[to_additive]
theorem le_minOrder_iff_forall_subgroup {n : ℕ∞} :
n ≤ minOrder G ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (s : Set G).Finite → n ≤ Nat.card s :=
by
rw [le_minOrder]
refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩
· obtain ⟨a, has, ha⟩ := s.bot_or_exists_ne_one.resolve_left hs
exact
(h ha <| finite_zpowers.1 <| hs'.subset <| zpowers_le.2 has).trans
(WithTop.coe_le_coe.2 <| s.orderOf_le_card hs' has)
· simpa using h (zpowers_ne_bot.2 ha) ha'.finite_zpowers
