truncate_truncate — Mathlib

English

For n1 ≤ n2 ≤ n3, (truncate n1) (truncate n2 x) = truncate (n1 ∘ n2) x for x ∈ TruncatedWittVector p n3 R.

Русский

Для n1 ≤ n2 ≤ n3 верно: (truncate n1)(truncate n2 x) = truncate (n1.trans n2) x для x ∈ TruncatedWittVector p n3 R.

LaTeX

$$$$ (\\operatorname{truncate} n1) (\\operatorname{truncate} n2 x) = \\operatorname{truncate} (n1 \\mathbin{.} n2) x. $$$$

Lean4

@[simp]
theorem truncate_truncate {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃) (x : TruncatedWittVector p n₃ R) :
    (truncate h1) (truncate h2 x) = truncate (h1.trans h2) x :=
  by
  obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) n₃ R x
  simp only [truncate_wittVector_truncate]

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