isCompl_iff — Mathlib

English

IsCompl for p q in Subtype equals IsCompl for p and q in Submodules.

Русский

IsCompl для p,q в подтипе равно IsCompl для p и q в подмодулях.

LaTeX

$${p q : f.invtSubmodule} \; IsCompl p q \iff IsCompl (p : Submodule R M) (q : Submodule R M)$$

Lean4

protected theorem isCompl_iff {p q : f.invtSubmodule} : IsCompl p q ↔ IsCompl (p : Submodule R M) (q : Submodule R M) :=
  by
  obtain ⟨p, hp⟩ := p
  obtain ⟨q, hq⟩ := q
  simp

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