trans — Mathlib

English

If n and m are natural numbers and R,S,T form the right towers, then the relative dimension is additive: relDim(R,T) = m+n.

Русский

Если n и m — натуральные числа, и R,S,T образуют нужную башню, то относительная размерность суммируется: relDim(R,T) = n+m.

LaTeX

$$$\mathrm{relDim}(R,T) = \mathrm{relDim}(R,S) + \mathrm{relDim}(S,T)$$$

Lean4

theorem trans [IsStandardSmoothOfRelativeDimension n R S] [IsStandardSmoothOfRelativeDimension m S T] :
    IsStandardSmoothOfRelativeDimension (m + n) R T where
  out := by
    obtain ⟨_, _, _, _, P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
    obtain ⟨_, _, _, _, Q, hQ⟩ := ‹IsStandardSmoothOfRelativeDimension m S T›
    refine ⟨_, _, _, inferInstance, Q.comp P, hP ▸ hQ ▸ ?_⟩
    apply PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

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