hasProd_subtype_comap_iff_of_mulSupport_subset

English

If mulSupport f is contained in s, HasProd (f ∘ (↑)) a (L.comap Embedding.subtype) is equivalent to HasProd f a L.

Русский

Если mulSupport f ⊆ s, HasProd (f ∘ (↑)) a (L.comap Embedding.subtype) эквивалентно HasProd f a L.

LaTeX

$$$ HasProd (f \circ (↑)) a (L.comap (Embedding.subtype _)) \leftrightarrow HasProd f a L $$$

Lean4

@[to_additive]
theorem hasProd_subtype_comap_iff_of_mulSupport_subset {s : Set β} (hf : mulSupport f ⊆ s) :
    HasProd (f ∘ (↑) : s → α) a (L.comap <| Embedding.subtype _) ↔ HasProd f a L :=
  Subtype.coe_injective.hasProd_comap_iff <| by simpa using mulSupport_subset_iff'.1 hf

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