minimalPeriod_eq_one_of_subsingleton

English

If α has at most one element (is a singleton), then for any f: α → α and any x ∈ α, the minimal period of x is 1.

Русский

Пусть α имеет не более одного элемента (одиночный тип). Тогда для любой функции f: α → α и любого x ∈ α минимальный период x равен 1.

LaTeX

$$$\\forall f:\\alpha \\to \\alpha,\\ \\forall x:\\alpha,\\ \\operatorname{minimalPeriod}(f,x)=1$$$

Lean4

@[nontriviality]
theorem minimalPeriod_eq_one_of_subsingleton [Subsingleton α] : minimalPeriod f x = 1 := by simp [nontriviality]

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