propertyIsLocal — Mathlib

English

Smoothness is a local property.

Русский

Гладкость является локальным свойством.

LaTeX

$$$\mathrm{PropertyIsLocal}(\mathrm{Smooth})$$$

Lean4

/-- Smoothness is a local property of ring homomorphisms. -/
theorem propertyIsLocal : PropertyIsLocal Smooth
    where
  localizationAwayPreserves := isStableUnderBaseChange.localizationPreserves.away
  ofLocalizationSpanTarget := ofLocalizationSpanTarget
  ofLocalizationSpan :=
    ofLocalizationSpanTarget.ofLocalizationSpan
      (stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).left
  StableUnderCompositionWithLocalizationAwayTarget :=
    (stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).right

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