head_eq_none_iff

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.head_eq_none_iff

English

Let s be a sequence. The head of s is none if and only if s is the empty sequence.

Русский

Пусть s — последовательность. Голова s равна none тогда и только тогда, когда s = nil.

LaTeX

$$$ head(s) = \\mathrm{none} \\iff s = \\mathrm{nil} $$$

Lean4

@[simp]
theorem head_eq_none_iff {s : Seq α} : s.head = none ↔ s = nil :=
  by
  constructor
  · apply head_eq_none
  · intro h
    simp [h]

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

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

Разделы

Аффилиация

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