source_restr_subset_source — Mathlib

English

For e: Dom(e) ⊆ α and S ⊆ α, the domain of e|_S is a subset of Dom(e).

Русский

Для частичного биективного отображения e с областью определения Dom(e) и подмножества S ⊆ α, область определения ограничения e|_S ⊆ Dom(e).

LaTeX

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

Lean4

theorem source_restr_subset_source (s : Set α) : (e.restr s).source ⊆ e.source :=
  inter_subset_left

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