val_restrict_apply — Mathlib

English

The restricted map value equals the original map value after restriction, i.e., the restriction preserves the image.

Русский

Значение ограниченного отображения совпадает со значением исходного отображения после ограничения.

LaTeX

$$$(h.restrict f s t x : β) = f x$$$

Lean4

@[simp]
theorem val_restrict_apply (h : MapsTo f s t) (x : s) : (h.restrict f s t x : β) = f x :=
  rfl

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