of_quotient_finiteDimensional — Mathlib

English

If the quotient E/p is finite dimensional and p is closed, then p is ClosedComplemented.

Русский

Если факторпространство E/p конечно размерно и p замкнуто, то p является ClosedComplemented.

LaTeX

$$p.ClosedComplemented$$

Lean4

theorem of_quotient_finiteDimensional [CompleteSpace 𝕜] [FiniteDimensional 𝕜 (E ⧸ p)] (hp : IsClosed (p : Set E)) :
    p.ClosedComplemented := by
  obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
  haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
  exact .of_isCompl_isClosed hq hp q.closed_of_finiteDimensional

Похожие утверждения