instFintypeSubtypeMemOfDecidablePred

English

If K is a subgroup of G and G is finite, then a suitable subtype of K is finite (Fintype).

Русский

Если K — подгруппа G и G конечна, тогда некоторый подпредставитель K является конечным (Fintype).

LaTeX

$$$K \\subseteq G$ и $|G| < \\infty \\Rightarrow |K| < \\infty$$$

Lean4

@[to_additive]
instance (K : Subgroup G) [DecidablePred (· ∈ K)] [Fintype G] : Fintype K :=
  show Fintype { g : G // g ∈ K } from inferInstance

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