codRestrictOfInjective_comp_apply

English

A bilinear map restricted to a subspace of the target and composed with an inclusion yields a bilinear map respecting the subspaces.

Русский

Две линейно-биективные операции совместно дают би-линейное отображение, сохраняющее подпространства.

LaTeX

$$$i \\circ (f)_{\\text{codRestrict}} = f$ in the bilinear setting; more precisely, the composed map equals the original bilinear map on restricted domains.$$

Lean4

@[simp]
theorem codRestrictOfInjective_comp_apply (x : M₁) : i (LinearMap.codRestrictOfInjective f i hi hf x) = f x := by
  simp [LinearMap.codRestrictOfInjective]

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