is_compact.nonempty_inter_of...

Stream: Is there code for X?

[Adam Topaz]

Do we have a variant of docs#is_compact.nonempty_Inter_of_directed_nonempty_compact_closed which instead of assuming that the collection of sets is directed instead assumes that the intersection of any finite subcollection of the sets is nonempty?

[Kevin Buzzard]

This is the contrapositive of "every open cover has a finite subcover" right?

[Adam Topaz]

Oh it's called docs#is_compact.inter_Inter_nonempty

[Kevin Buzzard]

(...so I was going to suggest looking near is_compact.elim_finite_subcover)

[Adam Topaz]

Yeah that's exactly the code for this inter_Inter_nonempty. Who comes up with these names :rofl: ?