English
For a function f and a set s, Multipliable (f restricted to s via embedding) is equivalent to Multipliable on the s.mulIndicator f function; the two notions of multipliability agree when restricting to the subtype defined by s.
Русский
Для функции f и множества s мультиплируемость функции f на подмножестве s совпадает с мультиплируемостью функции s.mulIndicator f; две концепции совпадают при ограничении к подмножеству, задаваемому s.
LaTeX
$$$\text{Multipliable } (f\circ (↑) : s \to α) \iff \text{Multipliable } (s.mulIndicator f)$$$
Lean4
@[to_additive]
theorem hasProd_subtype_iff_mulIndicator {s : Set β} : HasProd (f ∘ (↑) : s → α) a ↔ HasProd (s.mulIndicator f) a := by
rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]
