eval_lift — Mathlib

English

For a family of quotient maps f and a coherent system h, the nth evaluation after lifting equals f(n).

Русский

Для семейства отображений на частичные тождества f и согласованной системы h н-ая ступень после подъема совпадает с f(n).

LaTeX

$$$\mathrm{eval}_{I,N}(n) \circ \mathrm{lift}_{I} f\, h = f(n)$$$

Lean4

@[simp]
theorem eval_lift (f : ∀ (n : ℕ), M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N))
    (h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) : eval I N n ∘ₗ lift I f h = f n :=
  rfl

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