restr_eq_of_source_subset — Mathlib

English

Another formulation: if e.source ⊆ s then restricting e to s yields e.

Русский

Еще одно выражение: если e.source ⊆ s, то ограничение e до s дает e.

LaTeX

$${e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source \\subseteq s) : e.restr s = e$$

Lean4

theorem restr_eq_of_source_subset {e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source ⊆ s) : e.restr s = e :=
  toPartialEquiv_injective <| PartialEquiv.restr_eq_of_source_subset <| interior_maximal h e.open_source

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