Intersection of a collection of sets

Stream: new members

[Logan Johnson]

Hello, I am trying to work through some topology problems, and I was having an issue figuring out how to represent the intersection of a collection of topologies. My main goal is to show that some topology is equal to the intersection of a collection of other topologies and I want sure how I could possibly write out the intersection. I am currently trying to write out the problem like this:

example {γ} (A R : Set (Set γ)) (T Tₐ : TopologicalSpace γ) (C : Set (Set (Set γ)))
    (h1 : Tₐ = TopologicalSpace.generateFrom A) (h2 : ∀ T ∈ C, A ⊆ T) (h3 : R = ) : Tₐ = R :=

Would writing some h3 defining R to be the intersection of all topologies in C be the best way to approach this, and if so, how would I even express this? I have the proof written out fine on paper, but I really just don't know how to begin getting this in lean.

[Patrick Massot]

What is the pen and paper version of the lemma you are trying to state?

[Logan Johnson]

Show that if A is a basis for a topology on X , then the topology generated by A equals the intersection of all topologies on X that contain A.
This is exercise 5 from the basis section in Munkres' Topology.

[Patrick Massot]

This is very far from what you started to state.

[Patrick Massot]

For instance Tₐ = TopologicalSpace.generateFrom A does not say that A is a basis of anything.

[Logan Johnson]

Would 'TopologicalSpace.IsTopologicalBasis.eq_generateFrom` be something more along the lines of what I am looking for in this case?

[Julian Berman]

moogle.ai seems to do a good job of finding the right thing here I think. I put in the exercise unchanged, and it finds TopologicalSpace.isTopologicalBasis_of_subbasis and says If a family of sets s generates the topology, then intersections of finite subcollections of s form a topological basis.

[Julian Berman]

You can of course save from cheating by looking at the proof but maybe the statement helps.

[Patrick Massot]

Julian, this is not the statement Logan is asking for.

[Patrick Massot]

But yes, docs#TopologicalSpace.IsTopologicalBasis is relevant.

[Julian Berman]

Ah indeed sorry, I just reread it a second time.

[Patrick Massot]

@Logan Johnson the statement you want is:

example {X : Type*} [T : TopologicalSpace X] {A : Set (Set X)} (hA : IsTopologicalBasis A) :
    T = sSup {S : TopologicalSpace X | A ⊆ S.IsOpen}

[Patrick Massot]

I don't think it appears in Mathlib since it isn't useful for anything but making an exercises. But relevant facts if you want to prove it include docs#TopologicalSpace.IsTopologicalBasis.isOpen_iff, docs#isOpen_iff_mem_nhds, docs#setOf_isOpen_sSup, docs#mem_nhds_iff.

[Logan Johnson]

Thanks for the help! I'll try to get to work with this.

[Patrick Massot]

An important point to keep in mind is that the natural order relation on TopologicalSpace X is not inclusion, it is the opposite. So the sSup that appears in the above statement is indeed the intersection of those topologies seen as collections of sets.

[Luigi Massacci]

I was just about to ask why it was sSup and not sInf

[Kevin Buzzard]

T1 <= T2 iff id : (X,T1) -> (X,T2) is continuous, i.e. iff T1 has more opens than T2 :-)