isChain_replicate_of_rel — Mathlib

English

If a relation r satisfies r(a,a), then the constant list consisting of n copies of a is an r-chain for every n.

Русский

Если для элемента a верно r(a,a), то список, состоящий из n копий a, является r-цепью для любого n.

LaTeX

$$$\\forall a:\\alpha,\\ (r\\ a\\ a)\\Rightarrow\\forall n:\\mathbb{N},\\ IsChain r(\\text{replicate } n\\ a)$$$

Lean4

theorem isChain_replicate_of_rel (n : ℕ) {a : α} (h : r a a) : IsChain r (replicate n a) := by
  induction n using Nat.twoStepInduction <;> grind

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