English
If for every i, the image of f_i lies inside a subgroup s of N, then the image of lift f lies inside s as well.
Русский
Если для каждой i образ отображения f_i лежит внутри подгруппы s в N, тогда образ lift f тоже лежит внутри s.
LaTeX
$$$ (\\mathrm{lift} f).\\mathrm{range} \\le s \\quad\\text{given } \\forall i, (f_i).\\mathrm{range} \\le s$$
Lean4
theorem lift_range_le {N} [Group N] (f : ∀ i, G i →* N) {s : Subgroup N} (h : ∀ i, (f i).range ≤ s) :
(lift f).range ≤ s := by
rintro _ ⟨x, rfl⟩
induction x using CoprodI.induction_on with
| one => exact s.one_mem
| of i x =>
simp only [lift_of]
exact h i (Set.mem_range_self x)
| mul x y hx hy =>
simp only [map_mul]
exact s.mul_mem hx hy
