flatten

Mathlib.Data.List.Infix

URI: https://scilib.ai/kg/mathlib#List.IsInfix.flatten

Lean4

@[gcongr]
protected theorem flatten {l₁ l₂ : List (List α)} (h : l₁ <:+: l₂) : l₁.flatten <:+: l₂.flatten :=
  by
  rcases h with ⟨l, l', rfl⟩
  simp

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

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

Разделы

Аффилиация

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