erange_coe

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Module.erange_coe

English

Again, surjectivity of f implies injectivity of f.dualMap.

Русский

Опять же, сюръективность f влечёт инъективность f.dualMap.

LaTeX

$$$$ \\text{Surj}(f) \\Rightarrow \\text{Inj}(f^*). $$$$

Lean4

theorem erange_coe : LinearMap.range (eval R M) = ⊤ :=
  range_eq_top.mpr (bijective_dual_eval _ _).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru