equivProdOfSurjectiveOfIsCompl_apply

English

The evaluation of the product equivalence on a vector x is simply (f x, g x).

Русский

Применение эквивалентности произведения к вектору x равно (f x, g x).

LaTeX

$$$$\text{equivProdOfSurjectiveOfIsCompl}\; f\; g\; hf\; hg\; hfg\; x = (f x, g x).$$$$

Lean4

@[simp]
theorem equivProdOfSurjectiveOfIsCompl_apply {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : range f = ⊤) (hg : range g = ⊤)
    (hfg : IsCompl (ker f) (ker g)) (x : E) : equivProdOfSurjectiveOfIsCompl f g hf hg hfg x = (f x, g x) :=
  rfl

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