equivProdOfSurjectiveOfIsCompl_apply

English

The action of the equivalence on x ∈ E is the pair (f x, g x).

Русский

Действие эквивалентности на x ∈ E даёт пару (f x, g x).

LaTeX

$$$(equivProdOfSurjectiveOfIsCompl f g hf hg hfg)\, x = (f x, g x).$$$

Lean4

@[simp]
theorem equivProdOfSurjectiveOfIsCompl_apply {f : E →ₗ[R] F} {g : E →ₗ[R] 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

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