apply_none

Mathlib.Combinatorics.HalesJewett

URI: https://scilib.ai/kg/mathlib#Combinatorics.Line.apply_none

English

If at index i the line gives none, then l x i equals x for any x.

Русский

Если на позиции i линия даёт none, то l x i = x.

LaTeX

$$$\\forall l:\\ Line\\,\\alpha\\,\\iota,\\forall x:\\alpha,\\forall i:\\iota,\\ l.idxFun(i) = \\mathrm{none} \\Rightarrow l\\,x\\,i = x.$$$

Lean4

theorem apply_none {α ι} (l : Line α ι) (x : α) (i : ι) (h : l.idxFun i = none) : l x i = x := by
  simp only [Option.getD_none, h, l.apply_def]

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

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

Разделы

Аффилиация

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