eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open

English

There exists a finite subcollection of basis elements whose union is U.

Русский

Существует конечная подподсборка элементов базиса, чья объединение равно U.

LaTeX

$$$ \exists s : Finset b, U = s.toSet.sUnion $$$

Lean4

theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open (b : Set (Set X)) (hb : IsTopologicalBasis b)
    (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) : ∃ s : Finset b, U = s.toSet.sUnion :=
  by
  have hb' : b = range (fun i ↦ i : b → Set X) := by simp
  rw [hb'] at hb
  choose s hs hU using eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U hUc hUo
  have : Finite s := hs
  let _ : Fintype s := Fintype.ofFinite _
  use s.toFinset
  simp [hU]

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