finiteType_isLocal — Mathlib

English

Finite type can be checked on the source via span to the target using localization.

Русский

Финитный тип можно проверить по источнику через охват к целевому объекту с использованием локализации.

LaTeX

$$$\text{FP via span source}$$$

Lean4

theorem finiteType_isLocal : PropertyIsLocal @FiniteType :=
  ⟨finiteType_localizationPreserves.away, finiteType_ofLocalizationSpanTarget,
    finiteType_ofLocalizationSpanTarget.ofLocalizationSpan
      (finiteType_stableUnderComposition.stableUnderCompositionWithLocalizationAway
          finiteType_holdsForLocalizationAway).left,
    (finiteType_stableUnderComposition.stableUnderCompositionWithLocalizationAway
        finiteType_holdsForLocalizationAway).right⟩

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