sublist — Mathlib

English

If l₂ is an IsChainR and l₁ is a sublist of l₂, then l₁ is an IsChainR.

Русский

Если l₂ является IsChain R, а l₁ является подпоследовательностью l₂, то l₁ также является IsChain R.

LaTeX

$$IsChain R l₂ → l₁.Sublist l₂ → IsChain R l₁$$

Lean4

protected theorem sublist [Trans R R R] (hl : l₂.IsChain R) (h : l₁ <+ l₂) : l₁.IsChain R :=
  by
  rw [isChain_iff_pairwise] at hl ⊢
  exact hl.sublist h

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