sublist — Mathlib

English

If a reduction from L1 to L2 exists, then the length of L2 is not greater than the length of L1.

Русский

Если существует редукция L1 → L2, то |L2| ≤ |L1|.

LaTeX

$$$(\text{Red}\,L_1\,L_2) \Rightarrow |L_2| \le |L_1|$$$

Lean4

/-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`. -/
@[to_additive /-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`. -/
    ]
protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
  @reflTransGen_of_transitive_reflexive _ (fun a b => b <+ a) _ _ _ (fun l => List.Sublist.refl l)
    (fun _a _b _c hab hbc => List.Sublist.trans hbc hab) (fun _ _ => Red.Step.sublist)

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