toHomeomorphOfContinuousOpen_apply

Mathlib.Topology.Homeomorph.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.toHomeomorphOfContinuousOpen_apply

← MathLib Explorer

English

The underlying function of e.toHomeomorphOfContinuousOpen h1 h2 equals e.

Русский

У функции, порождаемой e через ContinuousOpen, подстановка сохраняется как e.

LaTeX

$$$ \\mathrm{toHomeomorphOfContinuousOpen}(e,h_1,h_2) = e $$$

Lean4

@[simp]
theorem toHomeomorphOfContinuousOpen_apply (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) :
    ⇑(e.toHomeomorphOfContinuousOpen h₁ h₂) = e :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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