Commit 2025-08-22 19:40 550efc0b
View on Github →add instance CompleteSpace for a subtype with IsClosed instance (#28709)
add instance [CompleteSpace α] {s : Set α} [hs : IsClosed s] : CompleteSpace s.
motivation: Submodule.HasOrthogonalProjection.ofCompleteSpace takes CompleteSpace ↥K and it is convenient to have this instance so that any closed submodule in a Hilbert space HasOrthogonalProjection
There is already IsClosed.completeSpace_coe but it takes (hs : IsClosed) (explicitly) and many proofs use it, so for the moment I leave both of them.
discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60CompleteSpace.60.20for.20closed.20subtypes.20in.20a.20.60CompleteSpace.60