range_lift_le — Mathlib

English

The range of lift f is contained in the subgroup s given by a hypothesis on f.

Русский

Область значения lift f содержится в подгруппе s при соответствующем предположении на f.

LaTeX

$$$\\operatorname{range}(lift f) \\le s$ under $Set.range f \\subseteq s$$$

Lean4

@[to_additive]
theorem range_lift_le {s : Subgroup β} (H : Set.range f ⊆ s) : (lift f).range ≤ s :=
  by
  rintro _ ⟨⟨L⟩, rfl⟩
  exact
    List.recOn L s.one_mem fun ⟨x, b⟩ tl ih ↦
      Bool.recOn b (by simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih) (by simpa using s.mul_mem (H ⟨x, rfl⟩) ih)

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