Built with doc-gen4, running Lean4.
Bubbles () indicate interactive fragments: hover for details, tap to reveal contents.
Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus.
On Mac, use Cmdinstead of Ctrl.
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
! This file was ported from Lean 3 source module data.list.sections
! leanprover-community/mathlib commit 26f081a2fb920140ed5bc5cc5344e84bcc7cb2b2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
# 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.
open Nat Function