isComplete_map_iff — Mathlib

English

If the ambient ring hom σ is surjective, then for any submodule p, p.map f is complete in E₂ iff p is complete in E.

Русский

Если отображение σ сюръективно, то для подмодуля p имеет место эквивалентность полноты: p.map f полно в E₂ тогда и только тогда, когда p полно в E.

LaTeX

$$IsComplete(p.map f) \iff IsComplete(p)$$

Lean4

theorem isComplete_map_iff [RingHomSurjective σ₁₂] {p : Submodule R E} :
    IsComplete (p.map f.toLinearMap : Set E₂) ↔ IsComplete (p : Set E) :=
  isComplete_image_iff f

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