# Zulip Chat Archive

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

s...)

While I'm here, how come `set.mem_union`

, `set.mem_Union`

and `set.mem_sUnion`

are all `iff`

s, 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