coe_restrict — Mathlib

English

If g(0) = 0, then mapping through g commutes with restriction: (restrict f s).map g = (f.map g).restrict s, provided 0 maps to 0.

Русский

Если g(0) = 0, то отображение после ограничения совпадает с ограничением после отображения: (restrict f s).map g = (f.map g).restrict s.

LaTeX

$$$(f.restrict s).map g = (f.map g).restrict s\\quad\\text{when } g(0)=0.$$$

Lean4

@[simp]
theorem coe_restrict (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) : ⇑(restrict f s) = indicator s f := by
  classical rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

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