of_le — Mathlib

English

There is a canonical embedding LEInfty cast from Nat to WithTop ℕ∞ used to index levels of regularity.

Русский

Существует каноническое вложение LEInfty из Nat в WithTop ℕ∞, индексирующее уровни гладкости.

LaTeX

$$$(n: Nat) \mapsto (n : WithTop ℕ∞)$$$

Lean4

protected theorem of_le {m n : WithTop ℕ∞} (hmn : m ≤ n) [IsManifold I n M] : IsManifold I m M :=
  by
  have : HasGroupoid M (contDiffGroupoid m I) :=
    hasGroupoid_of_le (G₁ := contDiffGroupoid n I) (by infer_instance) (contDiffGroupoid_le hmn)
  exact mk' I m M

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