Improve a proof

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I've defined the following:

def IsProjection {X : Type*} (P: X → X): Prop := P = P ∘ P

def IsComplemented (X 𝕂: Type*) [RCLike 𝕂] [NormedAddCommGroup X] [NormedSpace 𝕂 X] (Y: Subspace 𝕂 X) : Prop :=
  ∃ (P: X →L[𝕂] X), IsProjection P ∧ LinearMap.range P = Y

And I want to prove this result:

theorem complemented_closed (X 𝕂: Type*) [RCLike 𝕂] [NormedAddCommGroup X] [NormedSpace 𝕂 X] (Y: Subspace 𝕂 X) :
  IsComplemented X 𝕂 Y → @IsClosed X _ Y

To do so, I've done this:

theorem complemented_closed (X 𝕂: Type*) [RCLike 𝕂] [NormedAddCommGroup X] [NormedSpace 𝕂 X] (Y: Subspace 𝕂 X) :
  IsComplemented X 𝕂 Y → @IsClosed X _ Y := by
    intro Ycomp
    rcases Ycomp with ⟨P, Pproj, ranPeqY⟩
    have eqran : LinearMap.range P = LinearMap.range (P.toLinearMap) := by
      rfl
    rw [← ranPeqY, eqran, range_of_projection_eq_ker Pproj]
    apply ker_closed
    apply @sub_continuous X X 𝕂
    · exact id_continuous
    · exact P.continuous

Where the proofs of the theorems range_of_projection_eq_ker, sub_continuous and id_continuous are here

However, I fell like all I've used is already proven but I can't find it or make it work properly. How can I improve this proof?

Thanks in advance

[Jireh Loreaux]

sub_continuous is docs#Continuous.sub, id_continuous can be obtained with continuous_id, and fun_prop can be used to prove some of these things (although it seems to want eta-expanded versions). Also, it's a bit strange to assume that M N are AddCommGroups but, R is only a Semiring.

[Jireh Loreaux]

Also, we have docs#LinearMap.IsProj

[Esteban Martínez Vañó]

Thanks for the documentation, that simplifies a lot what I was doing.