liftOfSurjective_apply — Mathlib

English

If hf is surjective and hd holds, then for all x ∈ A, liftOfSurjective hf hd (f x) = f(d x).

Русский

Если hf сюръективен и выполнено hd, то для любого x ∈ A выполняется liftOfSurjective hf hd (f x) = f(d x).

LaTeX

$$$\operatorname{liftOfSurjective}\ hf\ hd\ (f(x)) = f(d(x))\quad\text{for all } x\in A.$$$

Lean4

theorem liftOfSurjective_apply {f : F} (hf : Function.Surjective f) {d : Derivation R A A}
    (hd : ∀ x, f x = 0 → f (d x) = 0) (x : A) : Derivation.liftOfSurjective hf hd (f x) = f (d x) := by simp

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