Documentation

Mathlib.Data.List.Sections

List sections #

This file proves some stuff about List.sections (definition in Data.List.Defs). A section of a list of lists [l₁, ..., lₙ] is a list whose i-th element comes from the i-th list.

theorem List.mem_sections {α : Type u_1} {L : List (List α)} {f : List α} :
f L.sections List.Forall₂ (fun (x1 : α) (x2 : List α) => x1 x2) f L
theorem List.mem_sections_length {α : Type u_1} {L : List (List α)} {f : List α} (h : f L.sections) :
f.length = L.length
theorem List.rel_sections {α : Type u_1} {β : Type u_2} {r : αβProp} :
(List.Forall₂ (List.Forall₂ r) List.Forall₂ (List.Forall₂ r)) List.sections List.sections