toOpenPartialHomeomorph_coe

Mathlib.Analysis.Calculus.Implicit

URI: https://scilib.ai/kg/mathlib#ImplicitFunctionData.toOpenPartialHomeomorph_coe

English

The underlying function defining the open partial homeomorphism is the product map (f, g).

Русский

Функция, задающая открытый частичный гомеоморфизм, по существу есть произведение (f, g).

LaTeX

$$$$ (\phi.toOpenPartialHomeomorph)(x) = (\phi.leftFun x, \phi.rightFun x) $$$$

Lean4

@[simp]
theorem toOpenPartialHomeomorph_coe : ⇑φ.toOpenPartialHomeomorph = φ.prodFun :=
  rfl

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

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

Разделы

Аффилиация

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