dual_bijective_iff_bijective — Mathlib

English

The dual map is bijective iff the original map is bijective.

Русский

Дуальное отображение биективно тогда и только тогда, когда исходное отображение биективно.

LaTeX

$$$\mathrm{Bijective}(dual f) \iff \mathrm{Bijective}(f)$$$

Lean4

theorem dual_bijective_iff_bijective {f : A →ₗ[R] A'} : Function.Bijective (dual f) ↔ Function.Bijective f :=
  ⟨fun h ↦ ⟨dual_surjective_iff_injective.mp h.2, dual_injective_iff_surjective.mp h.1⟩, fun h ↦
    ⟨dual_injective_iff_surjective.mpr h.2, dual_surjective_iff_injective.mpr h.1⟩⟩

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