of_isInducing — Mathlib

English

If Y is prespectral and f : X → Y is inducing and IsSpectralMap, then X is prespectral.

Русский

Если Y prespectral, а f: X → Y индуцирующее и спектральное отображение, то X prespectral.

LaTeX

$$$[\\mathrm{PrespectralSpace}(Y)] \\land (f: X\\to Y) \\text{ inducing} \\land (f \\text{ isSpectralMap}) \\Rightarrow \\mathrm{PrespectralSpace}(X)$$$

Lean4

theorem of_isInducing [PrespectralSpace Y] (f : X → Y) (hf : IsInducing f) (hf' : IsSpectralMap f) :
    PrespectralSpace X :=
  .of_isTopologicalBasis (PrespectralSpace.isTopologicalBasis.isInducing hf)
    (by
      simp only [Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp]
      rintro _ U h₁ h₂ rfl
      exact hf'.isCompact_preimage_of_isOpen h₁ h₂)

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