restr_eq_of_source_subset — Mathlib

English

If Dom(e) ⊆ S, then restricting e to S yields the same partial bijection: e|_S = e.

Русский

Если Dom(e) ⊆ S, то ограничение e на S совпадает с e: e|_S = e.

LaTeX

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

Lean4

theorem restr_eq_of_source_subset {e : PartialEquiv α β} {s : Set α} (h : e.source ⊆ s) : e.restr s = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [inter_eq_self_of_subset_left h])

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