below_of_le — Mathlib

English

If l1 extends l and l2 extends l, and |l1| ≤ |l2|, then l1 extends l2.

Русский

Если l1 расширяет l и l2 расширяет l, и длины |l1| ≤ |l2|, то l1 расширяет l2.

LaTeX

$$$\\mathrm{BlankExtends}(l_1,l) \\land \\mathrm{BlankExtends}(l_2,l) \\land |l_1| \\le |l_2| \\Rightarrow \\mathrm{BlankExtends}(l_1,l_2).$$$

Lean4

theorem below_of_le {Γ} [Inhabited Γ] {l l₁ l₂ : List Γ} :
    BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂ :=
  by
  rintro ⟨i, rfl⟩ ⟨j, rfl⟩ h; use j - i
  simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h
  simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

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