English
For lists l1, l2 of α and a true-subset relation, l1 ⊆ l2 iff every element of l1.toList is in l2.
Русский
Для списков l1, l2 α и подмножества, l1 ⊆ l2 тогда и только тогда, когда каждый элемент l1.toList принадлежит l2.
LaTeX
$$$l_1 \\subseteq l_2 \\;\\iff\\; \\forall a \\in l_1.toList, a \\in l_2$$$
Lean4
theorem subset_def {l₁ l₂ : Lists' α true} : l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂ :=
⟨fun H _ => mem_of_subset' H, fun H =>
by
induction l₁ using recOfList with
| _ l₁
induction l₁ with
| nil => exact Subset.nil
| cons h t t_ih =>
simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
exact cons_subset.2 ⟨H.1, t_ih H.2⟩⟩
