restrict — Mathlib

English

If f is box-additive on I0, then restricting to a smaller I ≤ I0 yields a box-additive map on I.

Русский

Если f BoxAdditiveMap на I0, то ограничение до меньшего I ≤ I0 дает BoxAdditiveMap на I.

LaTeX

$$$\operatorname{restrict}(f, I, h) : ι →ᵇᵃ[I] M$$$

Lean4

/-- If `f` is box-additive on subboxes of `I₀`, then it is box-additive on subboxes of any
`I ≤ I₀`. -/
@[simps]
def restrict (f : ι →ᵇᵃ[I₀] M) (I : WithTop (Box ι)) (hI : I ≤ I₀) : ι →ᵇᵃ[I] M :=
  ⟨f, fun J hJ => f.2 J (hJ.trans hI)⟩

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