liftOn_mk — Mathlib

English

For any f: N × K → L and hf providing compatibility with R_K_p, the value of the lift at a canonical element mk(K, p, x) is exactly f(x).

Русский

Для любого f: N × K → L и hf, обеспечивающего совместимость с R_K_p, значение liftOn на каноническом элементе mk(K, p, x) равно f(x).

LaTeX

$$$\\forall K [\\text{CommRing }K], p, [\\text{Prime }p], [\\text{CharP }K p], {L}, (f: \\mathbb{N} \\times K \\to L) (hf: \\forall x y, R K p x y \\to f x = f y) (x: \\mathbb{N} \\times K), (mk K p x).liftOn f hf = f x$$$

Lean4

@[simp]
theorem liftOn_mk {L : Sort _} (f : ℕ × K → L) (hf : ∀ x y, R K p x y → f x = f y) (x : ℕ × K) :
    (mk K p x).liftOn f hf = f x :=
  rfl

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