isSemilinearSet_image_iff — Mathlib

English

For a bijective-like map f with equivalence class, IsSemilinearSet(f'' s) iff IsSemilinearSet s.

Русский

Для биективного отображения f выполняется эквивалентность: IsSemilinearSet(f'' s) ⇔ IsSemilinearSet s.

LaTeX

$$$IsSemilinearSet (f '' s) \iff IsSemilinearSet s$$$

Lean4

theorem isSemilinearSet_image_iff {F : Type*} [EquivLike F M N] [AddEquivClass F M N] (f : F) :
    IsSemilinearSet (f '' s) ↔ IsSemilinearSet s :=
  by
  constructor <;> intro h
  · convert h.image (f : M ≃+ N).symm
    simp [image_image]
  · exact h.image f

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