restr_source — Mathlib

English

Let e be a partial bijection between α and β and S ⊆ α. Then the domain of the restriction e|_S is Dom(e) ∩ S.

Русский

Пусть e — частичное биективное отображение между α и β, и S ⊆ α. Тогда область определения ограничения e|_S равна Dom(e) ∩ S.

LaTeX

$$$\operatorname{Dom}(e|_{S}) = \operatorname{Dom}(e) \cap S$$$

Lean4

@[simp, mfld_simps]
theorem restr_source (s : Set α) : (e.restr s).source = e.source ∩ s :=
  rfl

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