English
For a finite index set ι and a family of subspaces W_i ⊆ V, the dual annihilator of the infimum equals the supremum of the dual annihilators:
Русский
Для конечного множества индексов ι и семейства подпространств W_i ⊆ V дуальный аннигилятор пересечения равен сумме дуальных аннигиляторов.
LaTeX
$$$\\bigwedge_{i\\in ι} W_i^{\\perp} = \\bigvee_{i\\in ι} W_i^{\\perp}$$$
Lean4
theorem dualAnnihilator_iInf_eq {ι : Type*} [Finite ι] (W : ι → Subspace K V₁) :
(⨅ i : ι, W i).dualAnnihilator = ⨆ i : ι, (W i).dualAnnihilator :=
by
revert ι
apply Finite.induction_empty_option
· intro α β h hyp W
rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
· intro W
rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
· intro α _ h W
rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
