restrict_equiv — Mathlib

English

Restricting a partial map to a dense open subset of its domain yields a map equivalent to the original one.

Русский

Ограничение частичного отображения до плотной открытой подмножества области определения даёт отображение, эквивалентное исходному.

LaTeX

$$$\forall f: X\.PartialMap Y\;\forall U\in X^{\mathrm{Opens}}\;\forall hU: Dense(U)\;\forall hU': U \le f.domain,\ (f.restrict U\; hU\; hU').hom \;\equiv \; f.hom$$$

Lean4

theorem restrict_equiv (f : X.PartialMap Y) (U : X.Opens) (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) :
    (f.restrict U hU hU').equiv f :=
  ⟨U, hU, le_rfl, hU', by simp⟩

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