subtype — Mathlib

English

If f: β → α is Multipliable, then its restriction to any subset s ⊆ β is Multipliable when viewed as a function on s.

Русский

Если f: β → α суммируема, то её ограничение на произвольном подмножестве s ⊆ β трактуется как функция на s и также суммируема.

LaTeX

$$$$\\text{Multipliable}(f) \\rightarrow \\forall s \\subseteq \\beta,\\ \\text{Multipliable}(f \\circ \\mathrm{Subtype.val}).$$$$

Lean4

@[to_additive]
theorem subtype (hf : Multipliable f) (s : Set β) : Multipliable (f ∘ (↑) : s → α) :=
  hf.comp_injective Subtype.coe_injective

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