mapDomain_support — Mathlib

English

With decidable equality, the support of mapDomain is contained in the image of the support under f.

Русский

При разрешимой равенстве опора mapDomain содержится в образе опоры под отображением f.

LaTeX

$$(s.mapDomain f).support ⊆ s.support.image f$$

Lean4

theorem mapDomain_support [DecidableEq β] {f : α → β} {s : α →₀ M} : (s.mapDomain f).support ⊆ s.support.image f :=
  Finset.Subset.trans support_sum <|
    Finset.Subset.trans (Finset.biUnion_mono fun _ _ => support_single_subset) <| by rw [Finset.biUnion_singleton]

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