instStructureGroupoidOrderTop — Mathlib

English

Every structure groupoid is below the groupoid of all open partial homeomorphisms; the top structure is the groupoid of all open partial homeomorphisms.

Русский

Каждая структура-групоид ниже группы открытых частичных гомоморфизмов; максимумом является группа открытых частичных гомоморфизмов.

LaTeX

$$$\\text{top} := \\mathrm{continuousGroupoid}(H) \\quad\\text{and}\\quad \\text{le\_top} \\;: \\; \\forall a,b, \\ a \\le \\text{top}$$$

Lean4

/-- Every structure groupoid is contained in the groupoid of all open partial homeomorphisms. -/
instance instStructureGroupoidOrderTop : OrderTop (StructureGroupoid H)
    where
  top := continuousGroupoid H
  le_top _ _ _ := ⟨trivial, trivial⟩

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