single_apply_left — Mathlib

English

If f: α → β is injective, then applying the single-mapping to f x on the left commutes with f in the argument: single (f x) y (f z) = single x y z.

Русский

Если f: α → β инъективно, то применение операции single с аргументами f x и f z эквивалентно применению single к x и z: single (f x) y (f z) = single x y z.

LaTeX

$$$$\\forall f:\\alpha\\to\\beta\\;\\text{(injective)},\\; x,z\\in\\alpha,\\; y\\in M:\\quad \\text{single }(f x)\\, y\\, (f z)=\\text{single }x\\, y\\, z.$$$$

Lean4

theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α) (y : M) :
    single (f x) y (f z) = single x y z := by classical simp only [single_apply, hf.eq_iff]

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