mem_of_source_eq_empty — Mathlib

English

Any change of coordinates with empty source belongs to the C^n groupoid.

Русский

Любое отображение координат с пустым источником принадлежит к группойоду C^n.

LaTeX

$$$f \in contDiffGroupoid\; n\; I$ whenever $f$ has empty source$$

Lean4

/-- Any change of coordinates with empty source belongs to `continuousGroupoid`. -/
theorem mem_of_source_eq_empty (f : OpenPartialHomeomorph H H) (hf : f.source = ∅) : f ∈ continuousGroupoid H :=
  by
  rw [← contDiffGroupoid_zero_eq (I := I)]
  exact ContDiffGroupoid.mem_of_source_eq_empty f hf

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