English
Given a function f defined on vertices outside a finite set K, which is constant on adjacent vertices, there is a well-defined extension (lift) to a function on the components outside K; i.e., a map from G.ComponentCompl K to the target β that depends only on the values of f on representatives outside K.
Русский
Пусть дано функция f на вершинах вне конечного множества K, константная на смежных вершинах. Тогда существует корректное продолжение (подъём) на множество компонент вне K; т.е. есть отображение из G.ComponentCompl K в β, зависящее только от значений f на представителей вне K.
LaTeX
$$$$ \text{lift}: (\forall \{v\}, v \notin K \to \beta) \to (\forall \{v,w\}, hv:\ v\notin K, hw:\ w\notin K, G.Adj\ v\ w \to f hv = f hw) \to (G.ComponentCompl K \to \beta) $$$$
Lean4
/-- A `ComponentCompl` specialization of `Quot.lift`, where soundness has to be proved only
for adjacent vertices.
-/
protected def lift {β : Sort*} (f : ∀ ⦃v⦄ (_ : v ∉ K), β)
(h : ∀ ⦃v w⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw) : G.ComponentCompl K → β :=
ConnectedComponent.lift (fun vv => f vv.prop) fun v w p => by
induction p with
| nil => rintro _; rfl
| cons a q ih => rename_i u v w; rintro h'; exact (h u.prop v.prop a).trans (ih h'.of_cons)
