range_lift_eq_closure — Mathlib

English

The range of lift f equals the closure of the range of f inside the appropriate subgroup.

Русский

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

LaTeX

$$$\\operatorname{range}(lift f) = \\operatorname{closure}(\\operatorname{range}(f))$$$

Lean4

@[to_additive]
theorem range_lift_eq_closure : (lift f).range = Subgroup.closure (Set.range f) :=
  by
  apply le_antisymm (range_lift_le Subgroup.subset_closure)
  rw [Subgroup.closure_le]
  rintro _ ⟨a, rfl⟩
  exact ⟨FreeGroup.of a, by simp only [lift_apply_of]⟩

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