linearMapOfTendsto — Mathlib

English

There exists a linear map built from a function approximated by closure of a range of linear maps, equipping it with a smul-preserving structure.

Русский

Существуют линейные карты, построенные из функции, аппроксимируемой замыканием образа линейных отображений, сохраняющие умножение на скаляры.

LaTeX

$$$\text{linearMapOfMemClosureRangeCoe}$$$

Lean4

/-- Construct a bundled linear map from a pointwise limit of linear maps -/
@[simps! -fullyApplied]
def linearMapOfTendsto (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [l.NeBot] (h : Tendsto (fun a x => g a x) l (𝓝 f)) :
    M₁ →ₛₗ[σ] M₂ :=
  linearMapOfMemClosureRangeCoe f <| mem_closure_of_tendsto h <| Eventually.of_forall fun _ => Set.mem_range_self _

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