domRestrict — Mathlib

English

Restriction of a partial equivalence to a substructure A of the domain, provided A ≤ dom(f).

Русский

Ограничение частичной эквивалентности до подструктуры A области определения, если A ⊆ dom(f).

LaTeX

$$$\text{domRestrict}(f,A,h)\;: M \equiv_p^L N$ with\ dom = A,\ cod = g.\text{range},\; \text{toEquiv} = g.\text{equivRange}$ where $g := (\operatorname{subtype} _).\circ (f. toEquiv. toEmbedding.\circ (A. inclusion(h)))$$$

Lean4

/-- Restriction of a partial equivalence to a substructure of the domain. -/
noncomputable def domRestrict (f : M ≃ₚ[L] N) {A : L.Substructure M} (h : A ≤ f.dom) : M ≃ₚ[L] N :=
  by
  let g := (subtype _).comp (f.toEquiv.toEmbedding.comp (A.inclusion h))
  exact
    { dom := A
      cod := g.toHom.range
      toEquiv := g.equivRange }

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