English
If U is compact-open covered and each X_i has a basis of compact opens with the IsCompact condition, then U can be expressed as a union of images of basis elements via appropriate indices.
Русский
Если U покрыто компактно-открыто и каждый X_i имеет базис компактно открытых множеств, при этом соблюдаются условия компактности, то U может быть выражено как объединение образов базисных элементов.
LaTeX
$$$\exists n\;\exists a: Fin n \to ι\;\exists V: \forall i, Opens (X (a i)), (\forall i, V i ∈ B (a i)) \land \bigcup_i f (a i) '' V i = U.$$$
Lean4
/-- If `U` is compact-open covered and the `X i` have a basis of compact opens,
`U` can be written as the union of images of elements of the basis. -/
theorem exists_mem_of_isBasis {B : ∀ i, Set (Opens (X i))} (hB : ∀ i, IsBasis (B i))
(hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.1) {U : Set S} (hU : IsCompactOpenCovered f U) :
∃ (n : ℕ) (a : Fin n → ι) (V : ∀ i, Opens (X (a i))), (∀ i, V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' V i = U :=
by
suffices h :
∃ (κ : Type _) (_ : Finite κ) (a : κ → ι) (V : ∀ i, Opens (X (a i))),
(∀ i, V i ∈ B (a i)) ∧ (∀ i, IsCompact (V i).1) ∧ ⋃ i, f (a i) '' V i = U
by
obtain ⟨κ, _, a, V, hB, hc, hU⟩ := h
cases nonempty_fintype κ
refine ⟨Fintype.card κ, a ∘ (Fintype.equivFin κ).symm, fun i ↦ V _, fun i ↦ hB _, ?_⟩
simp [← hU, ← (Fintype.equivFin κ).symm.surjective.iUnion_comp, Function.comp_apply]
obtain ⟨s, hs, V, hc, hunion⟩ := hU
choose Us UsB hUsf hUs using fun i : s ↦ (hB i.1).exists_finite_of_isCompact (hc i i.2)
let σ := Σ i : s, Us i
have : Finite s := hs
have (i : _) : Finite (Us i) := hUsf i
refine
⟨σ, inferInstance, fun i ↦ i.1.1, fun i ↦ i.2.1, fun i ↦ UsB _ (by simp), fun _ ↦ hBc _ _ (UsB _ (by simp)), ?_⟩
rw [← hunion]
ext x
simp_rw [Set.mem_iUnion]
refine ⟨fun ⟨i, hi, o, ho⟩ ↦ by aesop, fun ⟨i, hi, h, hmem, heq⟩ ↦ ?_⟩
rw [hUs ⟨i, hi⟩, coe_sSup, Set.mem_iUnion] at hmem
obtain ⟨a, ha⟩ := hmem
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at ha
use ⟨⟨i, hi⟩, ⟨a, ha.1⟩⟩, h, ha.2, heq
