continuousPregroupoid — Mathlib

English

The pregroupoid of all partial maps on a topological space H that arise from continuous data forms a Pregroupoid on H.

Русский

Пре-групоид всех частичных отображений на топологическом пространстве H, порождаемых непрерывными данными, образует прегрупоид на H.

LaTeX

$$$\\text{continuousPregroupoid}(H) \\text{ is a Pregroupoid on } H$$

Lean4

/-- The pregroupoid of all partial maps on a topological space `H`. -/
abbrev continuousPregroupoid (H : Type*) [TopologicalSpace H] : Pregroupoid H
    where
  property _ _ := True
  comp _ _ _ _ _ := trivial
  id_mem := trivial
  locality _ _ := trivial
  congr _ _ _ := trivial

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