imageOneHom — Mathlib

English

Lift a function to a OneHom via image; preserves one.

Русский

Поднять функцию в OneHom через image; сохраняет единицу.

LaTeX

$$imageOneHom f : OneHom (Finset α) (Finset β)$$

Lean4

/-- Lift a `OneHom` to `Finset` via `image`. -/
@[to_additive (attr := simps) /-- Lift a `ZeroHom` to `Finset` via `image` -/
    ]
def imageOneHom [DecidableEq β] [One β] [FunLike F α β] [OneHomClass F α β] (f : F) : OneHom (Finset α) (Finset β)
    where
  toFun := Finset.image f
  map_one' := by rw [image_one, map_one, singleton_one]

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