dual_injective_of_surjective — Mathlib

English

If f: A →ₗ[R] B is surjective, then the dual map dual f is injective.

Русский

Если f сюръективно отображает A в B, то дуальное отображение dual f инъективно.

LaTeX

$$Surjective f ⇒ Injective (dual f)$$

Lean4

theorem dual_injective_of_surjective (f : A →ₗ[R] B) (hf : Function.Surjective f) : Function.Injective (dual f) :=
  by
  intro φ ψ eq
  ext x
  obtain ⟨y, rfl⟩ := hf x
  change (dual f) φ _ = (dual f) ψ _
  rw [eq]

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