image — Mathlib

English

For any linear map f, the image f''s of a linear set s is linear.

Русский

Для любого линейного отображения f образ множества s линейный.

LaTeX

$$$IsLinearSet(s) \Rightarrow \forall f, IsLinearSet(f''s).$$$

Lean4

theorem image (hs : IsLinearSet s) (f : F) : IsLinearSet (f '' s) :=
  by
  rcases hs with ⟨a, t, ht, rfl⟩
  refine ⟨f a, f '' t, ht.image f, ?_⟩
  simp [image_vadd_distrib, ← AddMonoidHom.map_mclosure]

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