dual_surjective_iff_injective — Mathlib

English

Dual surjective iff dual injective; the conjunction yields a characterization of surjectivity and injectivity via duals.

Русский

Дуальное отображение сюръективно тогда и только тогда, когда инъективно; оба свойства связаны через двойственное отображение.

LaTeX

$$dual_surjective_iff_injective$$

Lean4

theorem dual_surjective_iff_injective {f : A →ₗ[R] A'} : Function.Surjective (dual f) ↔ Function.Injective f :=
  ⟨fun h ↦
    (injective_iff_map_eq_zero _).2 fun a h0 ↦
      eq_zero_of_character_apply fun c ↦ by obtain ⟨c, rfl⟩ := h c; exact congr(c $h0).trans c.map_zero,
    dual_surjective_of_injective f⟩

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