mapDomain_support_of_injective — Mathlib

English

If f is injective, the support equality holds: (mapDomain f s).support equals image f s.support.

Русский

Если f инъективна, то опора равна образу опоры: (mapDomain f s).support = image f s.support.

LaTeX

$$$\\text{mapDomain}_f s).\\text{support} = \\text{image} f s.\\text{support}$$$

Lean4

theorem mapDomain_support_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f) (s : α →₀ M) :
    (mapDomain f s).support = Finset.image f s.support :=
  mapDomain_support_of_injOn s hf.injOn

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