bijective_compr₂_of_equiv — Mathlib

English

Same as above, but g is a linear equivalence; this variant emphasizes the linear equivalence form.

Русский

То же самое, но здесь g является линейной эквивалентностью; подчеркивается форма линейной эквивалентности.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(f.compr₂ g.toLinearMap)$, $g : P \simeq Q$.$$

Lean4

/-- A version of `Function.Bijective.comp` for composition of a bilinear map with a linear map. -/
theorem bijective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Bijective f) :
    Bijective (f.compr₂ g.toLinearMap) :=
  ⟨injective_compr₂_of_injective f g.toLinearMap hf.1 g.bijective.1, surjective_compr₂_of_equiv f g hf.2⟩

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