dualAnnihilator_inj

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Subspace.dualAnnihilator_inj

← MathLib Explorer

English

If W^⊥ = (W')^⊥, then W = W'.

Русский

Если W^⊥ = (W')^⊥, то W = W'.

LaTeX

$$$W^{\perp} = (W')^{\perp} \Rightarrow W = W'$$$

Lean4

theorem dualAnnihilator_inj {W W' : Subspace K V} : W.dualAnnihilator = W'.dualAnnihilator ↔ W = W' :=
  ⟨fun h ↦ (dualAnnihilatorGci K V).l_injective h, congr_arg _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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