not_injective — Mathlib

English

A periodic function f: R → X with a nonzero period c ≠ 0 cannot be injective.

Русский

Периодическая функция f: R → X с непустым периодом c ≠ 0 не может быть инъективной.

LaTeX

$$$\forall R\,X\,[AddZeroClass R] \Rightarrow (f:R\to X)\ (hf:Periodic\ f\ c) (hc: c \neq 0) \rightarrow \lnot Injective\ f.$$$

Lean4

/-- A periodic function `f : R → X` on a semiring (or, more generally, `AddZeroClass`)
of non-zero period is not injective. -/
theorem not_injective {R X : Type*} [AddZeroClass R] {f : R → X} {c : R} (hf : Periodic f c) (hc : c ≠ 0) :
    ¬Injective f := fun h ↦ hc <| h hf.eq

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