a closed subset of a closed subset is closed (type problems)

Stream: maths

[Panagiotis Angelinos]

Hello! I am trying to prove that if T is a closed subset of S and S is a closed subset of X. I suspect this has already been done, but I cannot find it. The real reason that I am trying to do this is because it illustrates what my real question is. Here is what I have so far:

theorem closed_of_closed_implies_closed [TopologicalSpace X] {S : Set X} {T : Set ↑S}
  (hS : IsClosed S) (hT : IsClosed T) : IsClosed T := by sorry

Of course, this is not what I am supposed to do, since the second IsClosed T is supposed to assert that T : Set X is closed, but really it is saying that T : Set ↑S is closed (which is what the hypothesis says). From what I understand, a term of type Set ↑S is a term of type Set X along with a proof that T \subset S. I would like to know if there is some way to refer to the "underlying" term T : Set X, or more generally if I am going down the wrong path here.

[Edward van de Meent]

so your question is "what is the right return type"?

[Edward van de Meent]

you could possibly try making the arguments to the second IsClosed T more explicit, possibly along the lines of @IsClosed X _ T?

[Edward van de Meent]

or possibly @IsClosed X _ (T:Set X)?

[Panagiotis Angelinos]

Sorry, I am very new to this, and I don't know what you mean by "return type". The @IsClosed bit helped though, since there seems to have been some change in the tactics state. I'll see if I can make this work, thanks!

[Panagiotis Angelinos]

Well, this helped a lot! It seems to work, and in particular it helped me find the existing Lean code that proves it already! It also shows how to deal with my problem. Here's the code snippet for posterity.

variable [TopologicalSpace X] {s : Set X} {t : Set s}
theorem IsClosed.trans (ht : IsClosed t) (hs : IsClosed s) : IsClosed (t : Set X) := by
  rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩
  rw [Subtype.image_preimage_coe]
  exact hs.inter hs'

[Anatole Dedecker]

For the record, it could be golfed down to

variable [TopologicalSpace X] {s : Set X} {t : Set s}
theorem IsClosed.trans' (ht : IsClosed t) (hs : IsClosed s) : IsClosed (t : Set X) :=
  hs.closedEmbedding_subtype_val.isClosedMap t ht

[Patrick Massot]

Panagiotis Angelinos said:

From what I understand, a term of type Set ↑S is a term of type Set X along with a proof that T \subset S.

This is not correct.

[Kevin Buzzard]

A term of type ↑S is a term x of type X along with a proof that x \in S, but this doesn't generalise to Set ↑S.

[Michael Stoll]

x \in S, not x \in X.

[Kevin Buzzard]

Fixed -- thanks