pi_liftQ_eq_liftQ_pi — Mathlib

English

If M is infinite, then M ⧸ ⊥ is infinite.

Русский

Если M бесконечно, то M ⧸ ⊥ бесконечен.

LaTeX

$$$$ \\text{If } \\lvert M \\rvert = \\infty, \\text{ then } \\lvert M / \\{0\\} \\rvert = \\infty. $$$$

Lean4

theorem pi_liftQ_eq_liftQ_pi {ι : Type*} {N : ι → Type*} [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)]
    (f : (i : ι) → M →ₗ[R] (N i)) {p : Submodule R M} (h : ∀ i, p ≤ ker (f i)) :
    LinearMap.pi (fun i ↦ p.liftQ (f i) (h i)) = p.liftQ (LinearMap.pi f) (LinearMap.ker_pi f ▸ le_iInf h) :=
  by
  ext x i
  simp

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