Theorems · Theorem · general topology

IsCompactOpenCovered.of_comp

∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), PrespectralSpace (X i)] [inst_2 : TopologicalSpace S] {σ : Type u_4} {Y : σ → Type u_5}
  [inst_3 : (i : σ) → TopologicalSpace (Y i)] (g : (i : σ) → Y i → S) {a : σ → ι} (t : (i : σ) → Y i → X (a i)),
  (∀ (i : σ), Continuous (t i)) →
    (∀ (i : σ), g i = f (a i) ∘ t i) →
      (∀ (i : ι), Continuous (f i)) → ∀ {U : Set S}, IsOpen U → IsCompactOpenCovered g U → IsCompactOpenCovered f U

Being compact open covered descends along refinements if the spaces are prespectral.

Defined in

Mathlib.Topology.Sets.CompactOpenCovered

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpacePrespectralSpaceTopologicalSpaceTopologicalSpace