multipliable_subtype_iff_mulIndicator

English

For a set s, Multipliable (f restricted to s via Subtype) is equivalent to Multipliable (s.mulIndicator f).

Русский

Для множества s мультиплируемость (f, ограниченная на s через Subtype) эквивалентна мультиплируемости (s.mulIndicator f).

LaTeX

$$$\text{Multipliable } (f \circ (↑) : s \to α) \iff \text{Multipliable } (s.mulIndicator f)$$$

Lean4

@[to_additive]
theorem multipliable_subtype_iff_mulIndicator {s : Set β} :
    Multipliable (f ∘ (↑) : s → α) ↔ Multipliable (s.mulIndicator f) :=
  exists_congr fun _ ↦ hasProd_subtype_iff_mulIndicator

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