set U' : {U : Submodule K (ι → K) // U ≤ s.supportedFun K} := ⟨U,hU⟩
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
⊢ s.relOrthSpace (s.relOrthSpace U) = U
α : Type u_1
R✝ : Type u_2
η✝ : Type u_3
ι✝ : Type u_4
R : Type u_5
K : Type u_6
η : Type u_7
ι : Type u_8
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Fintype η
s : Set ι
hs : s.Finite
U : Submodule K (ι → K)
hU : U ≤ s.supportedFun K
U' : { U // U ≤ s.supportedFun K } := ⟨U, hU⟩
⊢ s.relOrthSpace (s.relOrthSpace U) = U