mk_eq_mk — Mathlib

English

The mk operation on AdicCauchySequence members preserves equality when indices align; the defining property gives mk (f.val n) = mk (f.val m) for m ≤ n.

Русский

Операция mk сохраняет равенство элементов при согласовании индексов; свойство задаёт mk (f.val n) = mk (f.val m) при m ≤ n.

LaTeX

$$$ \\forall m \\le n, \\; Submodule.Quotient.mk (p := (I^m \\cdot \\top)) (f.n) = Submodule.Quotient.mk (p := (I^m \\cdot \\top)) (f.m) $$$

Lean4

/-- The defining property of an adic Cauchy sequence unwrapped. -/
theorem mk_eq_mk {m n : ℕ} (hmn : m ≤ n) (f : AdicCauchySequence I M) :
    Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (f n) =
      Submodule.Quotient.mk (p := (I ^ m • ⊤ : Submodule R M)) (f m) :=
  (f.property hmn).symm

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