instCoeFunForallSet

Mathlib.Topology.ShrinkingLemma

URI: https://scilib.ai/kg/mathlib#ShrinkingLemma.PartialRefinement.instCoeFunForallSet

English

If c is a chain of partial refinements and i belongs to the carrier of some v in c, then find(c, ne, i) evaluated at i equals v(i).

Русский

Если c — цепь частичных уточнений и i принадлежит носителю некоторого v в c, то find(c, ne, i) для i равен v(i).

LaTeX

$$$\text{find}\ c\ ne\ i\ i = v\,i$$$

Lean4

instance : CoeFun (PartialRefinement u s p) fun _ => ι → Set X :=
  ⟨toFun⟩

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

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

Разделы

Аффилиация

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