restr_target — Mathlib

English

Let e: α ⇄ β and S ⊆ α. Then the target of e|_S is Ran(e) ∩ e.symm^{-1}(S).

Русский

Пусть e: α ⇄ β и S ⊆ α. Тогда целевая часть ограниченного отображения e|_S равна Ran(e) ∩ e.symm^{-1}(S).

LaTeX

$$$\operatorname{Ran}(e|_{S}) = \operatorname{Ran}(e) \cap e^{-1}_{\mathrm{symm}}(S)$$$

Lean4

@[simp, mfld_simps]
theorem restr_target (s : Set α) : (e.restr s).target = e.target ∩ e.symm ⁻¹' s :=
  rfl

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