topology without filters

Stream: Is there code for X?

[Kevin Buzzard]

I'm doing topology with the proofs I was taught, for pedagogical reasons.

The conclusion of docs#compact_iff_finite_subcover is (∃ (t : finset ι), s ⊆ ⋃ (i : ι) (H : i ∈ t), U i), which often turns into ⊢ x ∈ ⋃ (i : ι) (H : i ∈ t), U i. But my poor students cannot now rw mem_bUnion_iff because this is not a bUnion because t is a finset not a set :-(

Would the topologists welcome a PR proving

lemma compact_iff_finite_subcover'
  {α : Type} [topological_space α] {s : set α} :
  is_compact s ↔ (Π {ι : Type} (U : ι → (set α)), (∀ i, is_open (U i)) →
    s ⊆ (⋃ i, U i) → (∃ (t : set ι), t.finite ∧ s ⊆ (⋃ i ∈ t, U i))) :=
begin
  rw compact_iff_finite_subcover,
  split,
  { intros hs ι U hU hsU,
    cases hs U hU hsU with F hF,
    use [(↑F : set ι), finset.finite_to_set F],
    exact hF },
  { intros hs ι U hU hsU,
    rcases hs U hU hsU with ⟨F, hFfin, hF⟩,
    use hFfin.to_finset,
    convert hF,
    ext,
    simp }
end

? Sticking to sets makes the union stuff much easier for beginners (especially ones who have not been taught about finsets...)

While I'm here, how come set.mem_union, set.mem_Union and set.mem_sUnion are all iffs, but set.mem_bUnion isn't, and it's set.mem_bUnion_iff?

[Eric Wieser]

Can you rewrite by set.mem_Union twice?

[Yury G. Kudryashov]

I don't care whether we have a version of is_compact.elim* with set.finite or not. I mean, I'd merge a PR with this lemma but I don't think that this is important. BTW, it seems that we don't have {s : set α // finite s} ≃o finset α. If someone will PR this equivalence (either an equiv, or an order_iso), then please add more corollaries like docs#set.exists_finite_iff_finset. I can think of ∃, ∀, supr, infi.