quotientPiLift_mk — Mathlib

English

The canonical mk on the quotient of the product corresponds to the tuple of componentwise maps on each coordinate; i.e., quotientPiLift p f hf (Quotient.mk x) = (i ↦ f_i(x_i)).

Русский

Каноническое отображение, заданное на разложенном произведении, соответствует по координатам каждому компонентному отображению: Quotient.mk(x) через quotientPiLift даёт последовательность f_i(x_i).

LaTeX

$$$\\text{quotientPiLift}(p,f,hf)(\\Quotient.mk x) = (i \\mapsto f_i(x_i)).$$$

Lean4

@[simp]
theorem quotientPiLift_mk (p : ∀ i, Submodule R (Ms i)) (f : ∀ i, Ms i →ₗ[R] Ns i) (hf : ∀ i, p i ≤ ker (f i))
    (x : ∀ i, Ms i) : quotientPiLift p f hf (Quotient.mk x) = fun i => f i (x i) :=
  rfl

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