ClosedComplemented — Mathlib

English

If a submodule p is closed complemented, there exists a submodule q such that p and q form a direct complement and q is closed.

Русский

Если p замкнуто дополнен, существует q такое что p и q образуют прямое дополнение и q замкнут.

LaTeX

$$$$ \exists q \; IsClosed(q) \land IsCompl(p,q). $$$$

Lean4

/-- A submodule `p` is called *complemented* if there exists a continuous projection `M →ₗ[R] p`. -/
def ClosedComplemented (p : Submodule R M) : Prop :=
  ∃ f : M →L[R] p, ∀ x : p, f x = x

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