comp — Mathlib

English

If f: B → C and g: A → B are spectral maps, then their composition f ∘ g is a spectral map.

Русский

Если f: B → C и g: A → B — спектральные отображения, то их композиция f ∘ g является спектральным отображением.

LaTeX

$$$ IsSpectralMap(f) \land IsSpectralMap(g) \Rightarrow IsSpectralMap(f \circ g). $$$

Lean4

@[stacks 005B]
theorem comp {f : β → γ} {g : α → β} (hf : IsSpectralMap f) (hg : IsSpectralMap g) : IsSpectralMap (f ∘ g) :=
  ⟨hf.continuous.comp hg.continuous, fun _s hs₀ hs₁ =>
    ((hs₁.preimage_of_isOpen hf hs₀).preimage_of_isOpen hg) (hs₀.preimage hf.continuous)⟩

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