flip_surjective_iff₂

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#LinearMap.flip_surjective_iff₂

English

A second formulation of the infimum equality for dual annihilators across a family of subspaces.

Русский

Вторая формулировка равенства инфимумов дуальных аннигиляторов по семье подпространств.

LaTeX

$$(⋂ i, W_i)^{\\perp} = ⋁ i, W_i^{\\perp}$$

Lean4

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

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

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

Разделы

Аффилиация

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