dualAnnihilator_le_dualAnnihilator_iff

Mathlib.LinearAlgebra.Dual.Lemmas

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

← MathLib Explorer

English

For subspaces W, W' of V, W^⊥ ≤ (W')^⊥ if and only if W' ≤ W.

Русский

Для подпространств W, W' ⊆ V верно: W^⊥ ≤ (W')^⊥ тогда и только тогда, когда W' ≤ W.

LaTeX

$$$W^{\perp} \le (W')^{\perp} \iff W' \le W$$$

Lean4

theorem dualAnnihilator_le_dualAnnihilator_iff {W W' : Subspace K V} :
    W.dualAnnihilator ≤ W'.dualAnnihilator ↔ W' ≤ W :=
  (dualAnnihilatorGci K V).l_le_l_iff

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

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

Разделы

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

Аффилиация

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