eval_lift_apply — Mathlib

English

Evaluating the lifted Cauchy sequence at x yields the nth component of f applied to x: (lift I f h x).val n = f n x.

Русский

Оценка лифтом над элементом x возвращает n-ю компоненту: (lift I f h x).val n = f n x.

LaTeX

$$$(\mathrm{lift}\ I\ f\ h\ x).\mathrm{val}\ n = f(n)\,x$$$

Lean4

@[simp]
theorem eval_lift_apply (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 : ℕ) (x : M) :
    (lift I f h x).val n = f n x :=
  rfl

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