mathlib documentation

data.list.sections

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

theorem list.mem_sections_length {α : Type u} {L : list (list α)} {f : list α} :
f L.sectionsf.length = L.length

theorem list.rel_sections {α : Type u} {β : Type v} {r : α → β → Prop} :