compCLMOfContinuousLinearEquiv_apply

English

For a continuous linear equivalence g, and f ∈ 𝓢(E, F), the induced composition equals precomposition by g: compCLMOfContinuousLinearEquiv 𝕜 g f = f ∘ g.

Русский

Для непрерывной линейной эквивалентности g и f ∈ 𝓢(E, F) имеем: compCLMOfContinuousLinearEquiv 𝕜 g f = f ∘ g.

LaTeX

$$$compCLMOfContinuousLinearEquiv 𝕜 g f = f \circ g$$$

Lean4

@[simp]
theorem compCLMOfContinuousLinearEquiv_apply (g : D ≃L[ℝ] E) (f : 𝓢(E, F)) :
    compCLMOfContinuousLinearEquiv 𝕜 g f = f ∘ g :=
  rfl

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