restrict_eq_codRestrict — Mathlib

English

Reverse of codRestrict_restrict: restricting equals the codRestrict map with a suitable parameterization.

Русский

Обратное отношение codRestrict_restrict: ограничение эквивалентно codRestrict с подходящей параметризацией.

LaTeX

$$$h.restrict f s t = codRestrict (s.restrict f) t (fun x => h x.2)$$$

Lean4

/-- Reverse of `Set.codRestrict_restrict`. -/
theorem restrict_eq_codRestrict (h : MapsTo f s t) : h.restrict f s t = codRestrict (s.restrict f) t fun x => h x.2 :=
  rfl

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