flip_surjective_iff₁ — Mathlib

English

Under finite dimensionality, flip bijectivity is equivalent to bijectivity of the original map.

Русский

При конечном размерности разворот биективен тогда и только тогда, когда исходное отображение биективно.

LaTeX

$$$\\text{Bijective}(B^{\\mathrm{flip}}) \\iff \\text{Bijective}(B)$$$

Lean4

theorem flip_surjective_iff₁ [FiniteDimensional K V₁] : Surjective B.flip ↔ Injective B :=
  flip_injective_iff₂.symm

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