trans — Mathlib

English

If R→S and S→T are (relative) standard smooth, then R→T is standard smooth with dimension additivity.

Русский

Если R→S и S→T являются стандартно гладкими, то R→T гладко над R со сложением размерностей.

LaTeX

$$$\text{IsStandardSmooth}(R,S) \land \text{IsStandardSmooth}(S,T) \Rightarrow \text{IsStandardSmooth}(R,T)$$$

Lean4

theorem trans [IsStandardSmooth R S] [IsStandardSmooth S T] : IsStandardSmooth R T where
  out := by
    obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
    obtain ⟨_, _, _, _, ⟨Q⟩⟩ := ‹IsStandardSmooth S T›
    exact ⟨_, _, _, inferInstance, ⟨Q.comp P⟩⟩

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