leftCoset_cover_const_iff_surjOn — Mathlib

English

If a family of cosets covers the whole group, then at least one member subgroup has finite index.

Русский

Если семейство косет покрывает всю группу, то хотя бы одна из подгрупп имеет конечный индекс.

LaTeX

$$$\exists k \in s, (H k).FiniteIndex$$$

Lean4

@[to_additive]
theorem leftCoset_cover_const_iff_surjOn :
    ⋃ i ∈ s, g i • (H : Set G) = Set.univ ↔ Set.SurjOn (g · : ι → G ⧸ H) s Set.univ := by
  simp [Set.eq_univ_iff_forall, mem_leftCoset_iff, Set.SurjOn, QuotientGroup.forall_mk, QuotientGroup.eq]

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