take — Mathlib

English

If a sequence is an R-chain, then any initial segment taken from the front is also an R-chain.

Русский

Если последовательность образует цепь по отношению R, то любое начальное сечение слева также образует цепь.

LaTeX

$$$\\forall \\{\\alpha\\}, \\forall R:\\, \\alpha \\to \\alpha \\to \\mathrm{Prop}, \\forall l:\\, \\text{List }\\alpha,\\ IsChain\\, R\\, l \\rightarrow \\forall n:\\, \\mathbb{N}, \\ IsChain\\, R\\, (\\text{take } n\\, l) $$$

Lean4

theorem take (h : IsChain R l) (n : ℕ) : IsChain R (take n l) :=
  h.prefix (take_prefix _ _)

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