ofSet_trans' — Mathlib

English

Let e be an open partial homeomorphism between topological spaces X and Y, and let s be an open subset of X. Then composing the map ofSet s with e is the same as restricting e to the intersection of its source with s: (ofSet s hs).trans e = e.restr (e.source ∩ s).

Русский

Пусть e — открытое частичное гомеоморфизм X → Y, и s подмножество X открыто. Тогда композиция (ofSet s hs) с e равна ограничению e на пересечении его области определения с s: (ofSet s hs).trans e = e.restr (e.source ∩ s).

LaTeX

$$$ (OpenPartialHomeomorph.ofSet s hs).trans e = e.restr \left(e.source \cap s\right) $$$

Lean4

theorem ofSet_trans' {s : Set X} (hs : IsOpen s) : (ofSet s hs).trans e = e.restr (e.source ∩ s) := by
  rw [ofSet_trans, restr_source_inter]

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