English
If the family X_i has a basis of compact opens, then every compact-open covered set U can be written as a finite union of images of basis elements.
Русский
Если семейство X_i имеет базис компактно-открытых множеств, то любое U, покрытое компактно-открытым способом, можно записать как конечную объединение образов элементов базиса.
LaTeX
$$$\exists n, a: Fin n \to ι, V: \forall i, Opens(X (a i)),\; (\forall i, V i ∈ B (a i)) \land \bigcup_i f (a i)'' V i = U.$$$
Lean4
theorem iff_isCompactOpenCovered_sigmaMk :
IsCompactOpenCovered f U ↔ IsCompactOpenCovered (fun (_ : Unit) (p : Σ i : ι, X i) ↦ f p.1 p.2) U := by
classical
rw [iff_of_unique (ι := Unit)]
refine ⟨fun ⟨s, hs, V, hc, hU⟩ ↦ ?_, fun ⟨V, hc, heq⟩ ↦ ?_⟩
· refine ⟨⟨s.sigma fun i ↦ if h : i ∈ s then V i h else ∅, isOpen_sigma_iff.mpr ?_⟩, ?_, ?_⟩
· intro i
by_cases h : i ∈ s
· simpa [h] using (V _ _).2
· simp [h]
· dsimp only
exact Set.isCompact_sigma hs fun i ↦ (by simp_all)
· aesop
· obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq
have (i : ι) (hi : i ∈ s) : IsOpen (t i) :=
by
rw [← Set.mk_preimage_sigma (t := t) hi]
exact isOpen_sigma_iff.mp (heq' ▸ V.2) i
refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]
