surjective_compr₂_of_equiv — Mathlib

English

If f is surjective and g is a linear equivalence P ≃ Q, then f.compr₂ g is surjective.

Русский

Если f сюръективна и g — линейное эквивалентность P ≃ Q, то f.compr₂ g сюръективна.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(f.compr₂ g)$, где $g$ — эквивалентность $P \to Q$.$$

Lean4

/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
theorem surjective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Surjective f) :
    Surjective (f.compr₂ g.toLinearMap) :=
  surjective_compr₂_of_exists_rightInverse f g.toLinearMap hf ⟨g.symm, by simp⟩

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