isCompl_comap_subtype_of_isCompl_of_le

English

If q and r are complementary submodules of M and q ≤ p, then their pullbacks along the inclusion p → M are complementary inside p.

Русский

Если q и r — комплементарные подмодули M и q ⊆ p, то их прообраз под включением p → M образуют комплемент в p.

LaTeX

$$$IsCompl\bigl(q. comap\, p.{\text{subtype}}, r. comap\, p.{\text{subtype}}\bigr)$$

Lean4

theorem isCompl_comap_subtype_of_isCompl_of_le {p q r : Submodule R M} (h₁ : IsCompl q r) (h₂ : q ≤ p) :
    IsCompl (q.comap p.subtype) (r.comap p.subtype) := by
  simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂

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