𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (gramSchmidt 𝕜 b '' Set.Iio j) :=
  subset_span ((Set.mem_image _ _ _).2 ⟨i, hij, rfl⟩)
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
this : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (↑b '' Set.Iio j)
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
have : gramSchmidt 𝕜 b i ∈ span 𝕜 (b '' Set.Iio j) := by rwa [← span_gramSchmidt_Iio 𝕜 b j]
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝¹ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
this✝ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (↑b '' Set.Iio j)
this : ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)).support ⊆ Set.Iio j
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
this : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (↑b '' Set.Iio j)
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
have : ↑(b.repr (gramSchmidt 𝕜 b i)).support ⊆ Set.Iio j :=
  Basis.repr_support_subset_of_mem_span b (Set.Iio j) this
no goals
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this✝¹ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
this✝ : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (↑b '' Set.Iio j)
this : ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)).support ⊆ Set.Iio j
⊢ ↑(↑b.repr (gramSchmidt 𝕜 (↑b) i)) j = 0
exact (Finsupp.mem_supported' _ _).1 ((Finsupp.mem_supported 𝕜 _).2 this) j Set.not_mem_Iio_self
no goals
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i j : ι
hij : i < j
b : Basis ι 𝕜 E
this : gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (gramSchmidt 𝕜 ↑b '' Set.Iio j)
⊢ gramSchmidt 𝕜 (↑b) i ∈ span 𝕜 (↑b '' Set.Iio j)
rwa [← span_gramSchmidt_Iio 𝕜 b j]