empty — Mathlib

English

There exists a charted space structure on the empty type M over any H, given by vacuous maps.

Русский

Пусть M пустое; существует структура ChartedSpace H M через вакуумные отображения.

LaTeX

$$ChartedSpace.empty (H) (M)$$

Lean4

/-- An empty type is a charted space over any topological space. -/
def empty (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [IsEmpty M] : ChartedSpace H M
    where
  atlas := ∅
  chartAt x := (IsEmpty.false x).elim
  mem_chart_source x := (IsEmpty.false x).elim
  chart_mem_atlas x := (IsEmpty.false x).elim

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