mem_pullSub_short — Mathlib

English

For x,y with a length condition, y ∈ pullSub T x iff there exists z ∈ T with y = x ++ z.

Русский

При условии длины x и y верно: y ∈ pullSub T x тогда и только тогда, когда существует z ∈ T такое, что y = x ++ z.

LaTeX

$$$ x.length \\le y.length \\Rightarrow y \\in \\mathrm{pullSub}(T, x) \\iff \\exists z\\in T, y = x ++ z $$$

Lean4

theorem mem_pullSub_short (hl : y.length ≤ x.length) : y ∈ pullSub T x ↔ y <+: x ∧ [] ∈ T := by
  simp [pullSub, List.take_of_length_le hl, List.drop_eq_nil_iff.mpr hl]

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