instNonemptyElemListSubchain

Mathlib.Order.Height

URI: https://scilib.ai/kg/mathlib#Set.instNonemptyElemListSubchain

English

The subchain s.subchain is nonempty, i.e., there exists at least one element in it.

Русский

Подцепь s.subchain непустая; существует по крайней мере один элемент внутри неё.

LaTeX

$$$ \\exists l.\\ l \\in s.\\mathrm{subchain}. $$$

Lean4

instance : Nonempty s.subchain :=
  ⟨⟨[], s.nil_mem_subchain⟩⟩

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

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

Разделы

Аффилиация

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