case intro
R : Type u_2
inst✝⁸ : Ring R
M : Type u_1
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M₂ : Type ?u.2046866
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : TopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ IsClosed ↑p
R : Type u_2
inst✝⁸ : Ring R
M : Type u_1
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M₂ : Type ?u.2046866
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : TopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
h : ClosedComplemented p
⊢ IsClosed ↑p
rcases h with ⟨f, hf⟩
case intro
R : Type u_2
inst✝⁸ : Ring R
M : Type u_1
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M₂ : Type ?u.2046866
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : TopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
this : ker (ContinuousLinearMap.id R M - comp (subtypeL p) f) = p
⊢ IsClosed ↑p
case intro
R : Type u_2
inst✝⁸ : Ring R
M : Type u_1
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M₂ : Type ?u.2046866
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : TopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ IsClosed ↑p
have : ker (id R M - p.subtypeL.comp f) = p := LinearMap.ker_id_sub_eq_of_proj hf
no goals
case intro
R : Type u_2
inst✝⁸ : Ring R
M : Type u_1
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M₂ : Type ?u.2046866
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : TopologicalAddGroup M
inst✝ : T1Space M
p : Submodule R M
f : M →L[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
this : ker (ContinuousLinearMap.id R M - comp (subtypeL p) f) = p
⊢ IsClosed ↑p
exact this ▸ isClosed_ker _