no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2897691
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
ι' : Type ?u.2897743
ι'' : Type ?u.2897746
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type ?u.2897767
inst✝¹ : NormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (↑f ∘ v) ↔ Orthonormal 𝕜 v
classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2897691
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
ι' : Type ?u.2897743
ι'' : Type ?u.2897746
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type ?u.2897767
inst✝¹ : NormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (↑f ∘ v) ↔ Orthonormal 𝕜 v
simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]