coe_desc — Mathlib

English

The underlying function of the locally constant defined by desc is exactly the original function f, i.e., its coercion equals f.

Русский

Базовая функция, лежащая в основе локально константной функции, заданной через desc, равна исходной функции f.

LaTeX

$$$ \\text{coe}(\\mathrm{LocallyConstant.desc } f\\ h\\ cond\\ inj) = f $$$

Lean4

@[simp]
theorem coe_desc {X α β : Type*} [TopologicalSpace X] (f : X → α) (g : α → β) (h : LocallyConstant X β)
    (cond : g ∘ f = h) (inj : Function.Injective g) : ⇑(desc f h cond inj) = f :=
  rfl

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