ofList_subset — Mathlib

English

Every list is a subset of itself.

Русский

Каждый список является подмножеством самого себя.

LaTeX

$$$l \\subseteq l$$$

Lean4

theorem ofList_subset {l₁ l₂ : List (Lists α)} (h : l₁ ⊆ l₂) : Lists'.ofList l₁ ⊆ Lists'.ofList l₂ := by
  induction l₁ with
  | nil => exact Subset.nil
  | cons _ _ l₁_ih =>
    refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
    simp only [List.cons_subset] at h; simp [h]

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