## Stream: Is there code for X?

### Topic: topology without filters

#### 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))) :=
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 (Feb 09 2021 at 22:54):

Can you rewrite by set.mem_Union twice?

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