maximalAtlas_subset_of_le — Mathlib

English

If the order relation holds between ENat indices m ≤ n, then the corresponding maximal atlases satisfy the subset relation: maximalAtlas I n M ⊆ maximalAtlas I m M.

Русский

Если выполняется отношение порядка между индексами m ≤ n, то соответствующие максимальные атласы удовлетворяют вложению: maximalAtlas I n M ⊆ maximalAtlas I m M.

LaTeX

$$m \le n \Rightarrow maximalAtlas(I,n,M) ⊆ maximalAtlas(I,m,M)$$

Lean4

theorem maximalAtlas_subset_of_le {m n : WithTop ℕ∞} (h : m ≤ n) : maximalAtlas I n M ⊆ maximalAtlas I m M :=
  StructureGroupoid.maximalAtlas_mono (contDiffGroupoid_le h)

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