apply_some

Mathlib.Combinatorics.HalesJewett

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

English

If at index i the line gives some a, then l x i = a.

Русский

Если idxFun i = some a, то l x i = a.

LaTeX

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

Lean4

theorem apply_some (h : l.idxFun i = some a) : l x i = a := by simp [h]

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

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

Разделы

Аффилиация

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