contDiffGroupoid_le — Mathlib

English

If m ≤ n, then contDiffGroupoid n I ≤ contDiffGroupoid m I (more regularity implies inclusion).

Русский

Если m ≤ n, тогда contDiffGroupoid n I включается в contDiffGroupoid m I (более высокая гладкость включает меньшую).

LaTeX

$$$contDiffGroupoid n I \leq contDiffGroupoid m I$ when $m \le n$$$

Lean4

/-- Inclusion of the groupoid of `C^n` local diffeos in the groupoid of `C^m` local diffeos when
`m ≤ n` -/
theorem contDiffGroupoid_le (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I :=
  by
  rw [contDiffGroupoid, contDiffGroupoid]
  apply groupoid_of_pregroupoid_le
  intro f s hfs
  exact ContDiffOn.of_le hfs h

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