isOrderedSubsetOf

Mathlib.Tactic.FunProp.ToBatteries

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.isOrderedSubsetOf

Lean4

/-- Check if `a` can be obtained by removing elements from `b`. -/
def isOrderedSubsetOf {α} [Inhabited α] [DecidableEq α] (a b : Array α) : Bool :=
  Id.run
    (do
      if a.size > b.size then
        return false
      let mut i := 0
      for h' : j in [0:b.size]do
        if i = a.size then
          break
        if a[i]! = b[j] then
          i := i + 1
      if i = a.size then
        return true
      else
        return false)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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