mem_sections_length

Mathlib.Data.List.Sections

URI: https://scilib.ai/kg/mathlib#List.mem_sections_length

English

If f is a section of L, then the length of f equals the length of L.

Русский

Если f является секцией L, то длина f равна длине L.

LaTeX

$$$ \\forall L\\; \\forall f,\\ f \\in \\mathrm{sections}(L) \\Rightarrow \\mathrm{length}(f) = \\mathrm{length}(L).$$$

Lean4

theorem mem_sections_length {L : List (List α)} {f} (h : f ∈ sections L) : length f = length L :=
  (mem_sections.1 h).length_eq

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru