instOfNatWithTopENat — Mathlib

English

If the 0-th differentiability structure associated to a model with corners I on M is trivial (i.e., the contDiff groupoid at level 0 is the trivial one), then M carries a C^0-manifold structure modeled on I.

Русский

Если нулевой уровень структуры дифференциации, связанный с моделью с углами I на M, тривиален (contDiffGroupoid на уровне 0 совпадает с тривиальной группoidой), то M образует C^0-многообразие, моделируемое по I.

LaTeX

$$$\text{IsManifold}(I,0,M)$$$

Lean4

instance : IsManifold I 0 M :=
  by
  suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M
  constructor
  intro e e' he he'
  rw [contDiffGroupoid_zero_eq]
  trivial

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