Show that z is in a1

Stream: new members

[Shadman Sakib]

How do I prove that z in a vector space is an element of $a_1$ which is in a subspace R V?

[Shadman Sakib]

import analysis.complex.circle
import analysis.normed_space.inner_product

noncomputable theory

open complex
variables {V : Type*} [inner_product_space ℂ V]

example {V : Type u_1}
  [inner_product_space ℂ V]
  (a₁ : subspace ℝ V)
  [complete_space ↥a₁]
  (z : V) :
  z ∈ a₁ :=
begin
  admit,
end

[Eric Wieser]

What's the t argument doing there?

[Shadman Sakib]

Sorry, you are right, we do not need that

[Eric Wieser]

What's your maths proof?

[Eric Wieser]

Because this similar statement is obviously false:

example {V : Type u_1} [add_comm_monoid V] [module ℝ V]
  (a₁ : subspace ℝ V)
  (z : V) :
  z ∈ a₁ :=
begin
  -- false, pick `V = ℝ`, `a₁ = ⊥`, `z = 37`
end

[Shadman Sakib]

Z does not always have to be in $a_1$, but z can be on the line $a_1$; I do not have maths proof because I do not know how to prove this goal.

[Kyle Miller]

In math english your example is saying "For every subspace a_1 of a vector space V, and for every z in V, then z is in a_1." This is not in general true, unless we know more about a_1. What's the bigger picture of what you're trying to prove?

[Eric Rodriguez]

do you mean ∀ V, ∃ a₁ : subspace ℝ V, z ∈ a₁?

[Shadman Sakib]

Yeah @Eric Rodriguez that reflects what I'm trying to say much clearer

[Eric Wieser]

That means something very different though. The question is once again "what's your maths proof?".

[Shadman Sakib]

Sorry, I will get back to you

[Eric Wieser]

but z can be on the line $a_1$

This is your maths proof, right? "choose $a_1$ as the line through z, result is trivial"

[Eric Wieser]

Eric Rodriguez said:

do you mean ∀ V, ∃ a₁ : subspace ℝ V, z ∈ a₁?

Missing z, ∀ z : V, ∃ a₁ : subspace ℝ V, z ∈ a₁.

[Shadman Sakib]

I presume $a_1$ is a fixed line, since there is a specific $a_1 : subspace ℝ V$ given to us

[Eric Wieser]

"given to us" is not what "exists" means in the goal