source_eq

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.EqOnSource.source_eq

← MathLib Explorer

English

If e ≈ e' and f ≈ f' then e.trans f ≈ e'.trans f'.

Русский

Если e ≈ e' и f ≈ f', то e.trans f ≈ e'.trans f'.

LaTeX

$$$ (e \approx e') \land (f \approx f') \Rightarrow (e.trans f) \approx (e'.trans f') $$$

Lean4

/-- Two equivalent open partial homeomorphisms have the same source. -/
theorem source_eq {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.source = e'.source :=
  h.1

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

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

Разделы

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

Аффилиация

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