codRestrict — Mathlib

English

Restriction of a partial equivalence to a substructure A of the codomain.

Русский

Ограничение частичной эквивалентности до подструктуры A кодомы.

LaTeX

$$$\text{codRestrict}(f, A, h) := f^{-1}.\text{domRestrict}(...)^{-1}$$$

Lean4

/-- Restriction of a partial equivalence to a substructure of the codomain. -/
noncomputable def codRestrict (f : M ≃ₚ[L] N) {A : L.Substructure N} (h : A ≤ f.cod) : M ≃ₚ[L] N :=
  (f.symm.domRestrict h).symm

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