List sections #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem list.mem_sections {α : Type u_1} {L : list (list α)} {f : list α} :

f ∈ L.sections ↔ list.forall₂ has_mem.mem f L

source

theorem list.mem_sections_length {α : Type u_1} {L : list (list α)} {f : list α} (h : f ∈ L.sections) :

f.length = L.length

source

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