English
Let L be a list of lists. A list f belongs to sections L exactly when each element of f belongs to the corresponding sublist of L; i.e., f satisfies Forall₂ (λ x y, x ∈ y) with L.
Русский
Пусть L — список подсписков; список f принадлежит секциям L тогда и только тогда, когда каждый элемент f принадлежит соответствующему подсписку L, то есть выполняется Forall₂ (λ x y, x ∈ y) f L.
LaTeX
$$$ f \\in \\mathrm{sections}(L) \\iff \\mathrm{Forall_2}\\left(\\lambda x\\, y \\;\\mapsto\\; x \\in y\\right) (f)\\; L. $$$
Lean4
theorem mem_sections {L : List (List α)} {f} : f ∈ sections L ↔ Forall₂ (· ∈ ·) f L :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· induction L generalizing f
· cases mem_singleton.1 h
exact Forall₂.nil
simp only [sections, mem_flatMap, mem_map] at h
rcases h with ⟨_, _, _, _, rfl⟩
simp only [*, forall₂_cons, true_and]
·
induction h with
| nil => simp only [sections, mem_singleton]
| @cons a l f L al fL fs =>
simp only [sections, mem_flatMap, mem_map]
exact ⟨f, fs, a, al, rfl⟩
