eq_of_le_of_card_ge — Mathlib

English

Let H ≤ K be subgroups of G with K finite. If |K| ≤ |H|, then H = K.

Русский

Пусть H ≤ K — подгруппы G, K конечная. Если |K| ≤ |H|, тогда H = K.

LaTeX

$$$H \le K \quad [\text{Finite } K] \quad \text{and} \quad |K| \le |H| \;\Rightarrow\; H = K$$$

Lean4

@[to_additive]
theorem eq_of_le_of_card_ge {H K : Subgroup G} [Finite K] (hle : H ≤ K) (hcard : Nat.card K ≤ Nat.card H) : H = K :=
  SetLike.coe_injective <| Set.Finite.eq_of_subset_of_card_le (Set.toFinite _) hle hcard

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