restrict_range — Mathlib

English

The image of the restricted homomorphism f|K equals the image of K under f; i.e. (f|K).range = K.map f.

Русский

Образ ограниченного гомоморфизма f|K равен образу K под действием f.

LaTeX

$$$\mathrm{Im}(f|_K) = f(K)$$$

Lean4

@[to_additive (attr := simp)]
theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
  simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists, exists_prop, forall_const]

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