restr — Mathlib

English

If h is an image predicate, then the image of the restricted source under e equals the restricted target.

Русский

Если есть условие отображения, образ под ограничением совпадает с ограниченным целевым множеством.

LaTeX

$$e.IsImage s t → Set.image e.toFun (e.source ∩ s) = e.target ∩ t$$

Lean4

/-- Restrict a `PartialEquiv` to a pair of corresponding sets. -/
@[simps -fullyApplied]
def restr (h : e.IsImage s t) : PartialEquiv α β where
  toFun := e
  invFun := e.symm
  source := e.source ∩ s
  target := e.target ∩ t
  map_source' := h.mapsTo
  map_target' := h.symm_mapsTo
  left_inv' := e.leftInvOn.mono inter_subset_left
  right_inv' := e.rightInvOn.mono inter_subset_left

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