trans_of_set'

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.trans_of_set'

English

A variant of trans_ofSet equates e.trans (ofSet s hs) with restricting to e.source ∩ preimage s.

Русский

Вариант trans_ofSet: e.trans (ofSet s hs) = e.restr (e.source ∩ preimage s).

LaTeX

$$$ e.trans (\\mathrm{ofSet} s hs) = e.restr (e.source \\cap \\mathrm{preimage} e.toFun' s) $$$

Lean4

theorem trans_of_set' {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e.source ∩ e ⁻¹' s) := by
  rw [trans_ofSet, restr_source_inter]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru