isConstructible_preimage — Mathlib

English

For f: X → Y and s constructible in Y, the preimage f^{-1}(s) is constructible.

Русский

Для f: X → Y и s конструктивна во множестве Y, тогда предобраз f^{-1}(s) конструктивен.

LaTeX

$$$\forall f, \ IsConstructible(s) \Rightarrow \ IsConstructible(f^{-1}(s)).$$$

Lean4

@[stacks 054I]
theorem isConstructible_preimage (f : X.Hom Y) {s : Set Y} (hs : IsConstructible s) : IsConstructible (f.base ⁻¹' s) :=
  hs.preimage f.continuous fun t ht ht' ↦
    IsRetrocompact_iff_isSpectralMap_subtypeVal.mpr
      ((quasiCompact_iff_spectral _).mp
        (MorphismProperty.of_isPullback (P := @QuasiCompact) (isPullback_morphismRestrict f ⟨t, ht⟩)
          ((quasiCompact_iff_spectral _).mpr (IsRetrocompact_iff_isSpectralMap_subtypeVal.mp ht'))))

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