hasProd_subtype_iff_of_mulSupport_subset

English

If mulSupport f ⊆ s, then HasProd (f ∘ (↑)) a in the subtype is equivalent to HasProd f a.

Русский

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

LaTeX

$$$ HasProd (f \circ (↑)) a \leftrightarrow HasProd f a $$$

Lean4

@[to_additive]
theorem hasProd_subtype_iff_of_mulSupport_subset {s : Set β} (hf : mulSupport f ⊆ s) :
    HasProd (f ∘ (↑) : s → α) a ↔ HasProd f a := by
  simpa using hasProd_subtype_comap_iff_of_mulSupport_subset hf (L := unconditional _)

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