linear_surjective_iff — Mathlib

English

For an affine endomorphism f, f.linear is bijective if and only if f is bijective as a map.

Русский

Для аффинного эндоморфизма f линейная часть f.linear биективна тогда и только тогда, когда сам f биективен.

LaTeX

$$$\\mathrm{Bijective}(f.linear) \\;\\Leftrightarrow\\; \\mathrm{Bijective}(f)$$$

Lean4

@[simp]
theorem linear_surjective_iff (f : P1 →ᵃ[k] P2) : Function.Surjective f.linear ↔ Function.Surjective f :=
  by
  obtain ⟨p⟩ := (inferInstance : Nonempty P1)
  have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p :=
    by
    ext v
    simp [f.map_vadd]
  rw [h, Equiv.comp_surjective, Equiv.surjective_comp]

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