isStandardSmooth — Mathlib

English

From an IsStandardSmoothOfRelativeDimension object, one obtains IsStandardSmooth.

Русский

Из объекта IsStandardSmoothOfRelativeDimension следует получить IsStandardSmooth.

LaTeX

$$$\text{IsStandardSmoothOfRelativeDimension}(n,R,S) \Rightarrow \mathrm{IsStandardSmooth}(R,S)$$$

Lean4

theorem isStandardSmooth [H : IsStandardSmoothOfRelativeDimension n R S] : IsStandardSmooth R S :=
  ⟨_, _, _, H.out.choose_spec.choose_spec.choose_spec.choose,
    H.out.choose_spec.choose_spec.choose_spec.choose_spec.nonempty⟩

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