Zulip Chat Archive

Stream: Is there code for X?

Topic: topology without filters

view this post on Zulip Kevin Buzzard (Feb 09 2021 at 22:18):

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))) :=
  rw compact_iff_finite_subcover,
  { 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,
    simp }

? 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?

view this post on Zulip Eric Wieser (Feb 09 2021 at 22:54):

Can you rewrite by set.mem_Union twice?

view this post on Zulip Yury G. Kudryashov (Mar 02 2021 at 05:11):

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.

Last updated: May 17 2021 at 15:13 UTC