isEmpty_of_chartedSpace

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#isEmpty_of_chartedSpace

← MathLib Explorer

English

If H is empty, then M is empty.

Русский

Если H пусто, то и M пусто.

LaTeX

$$$\\text{IsEmpty}(H) \\Rightarrow \\text{IsEmpty}(M)$$$

Lean4

theorem isEmpty_of_chartedSpace (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M]
    [IsEmpty H] : IsEmpty M := by
  rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩
  · exact hM
  · exact (IsEmpty.false (chartAt H x x)).elim

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

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

Разделы

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

Аффилиация

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