𝕜 : Type u_1
E : Type u_2
F : Type ?u.2153778
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2153827
dec_ι : DecidableEq ι
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 fun x => ↑x
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2153778
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2153827
dec_ι : DecidableEq ι
⊢ Orthonormal 𝕜 fun x => ↑x
classical!
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2153778
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type ?u.2153827
dec_ι : DecidableEq ι
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 fun x => ↑x
simp [orthonormal_subtype_iff_ite]