restrict_commutes — Mathlib

English

Restricting a MapsTo relation commutes with function composition via the inclusion map.

Русский

Ограничение отношения MapsTo коммутирует с композицией функций через внедрение.

LaTeX

$$$Sub\\type{val} \\circ h.restrict f s t = f \\circ Sub\\type{val}$$$

Lean4

theorem restrict_commutes (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) :
    Subtype.val ∘ h.restrict f s t = f ∘ Subtype.val :=
  rfl

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