dual_injective_iff_surjective — Mathlib

English

Dual injective is equivalent to surjective; this is a restatement of dual_surjective_iff_injective.

Русский

Инъективность дуалa эквивалентна сюръективности; повторяет dual_surjective_iff_injective.

LaTeX

$$dual_injective_iff_surjective$$

Lean4

theorem dual_injective_iff_surjective {f : A →ₗ[R] A'} : Function.Injective (dual f) ↔ Function.Surjective f :=
  ⟨fun h ↦ surjective_of_dual_injective f h, fun h ↦ dual_injective_of_surjective f h⟩

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