Problem of closed set

Stream: new members

[haotian liu]

Is there a relevant theorem inside mathilb that accomplishes the proof of the following theorem? If not, is there a theorem that I can learn from?

have hdef_r_close {zset_r : Set ℝ} (hdef1 : zset_r = {x | (αleft ≤ x ∧ x ≤ αright)}) : IsClosed (zset_r) := by
      sorry

[Kyle Miller]

Yes, docs#isClosed_Icc

[haotian liu]

Thank you very much!
Actually, I want to prove the following problem:

private theorem Is_closed_zset {αleft αright : ℝ} {g : ℝ → ℝ} {zset : Set ℝ}
    (hdef : zset = {x | (αleft ≤ x ∧ x ≤ αright) ∧ g x = 0}) (hg : Continuous g) :
    IsClosed (zset) := by
    sorry

Now, I can prove that zset_r = {x | (αleft ≤ x ∧ x ≤ αright)} is closed.
Is there any theorem that proves that a subset of a closed set is also a closed set?
Or is there any theorem that proves that the set of zeros of a continuous function is a closed set?

[Kyle Miller]

theorem Is_closed_zset {αleft αright : ℝ} {g : ℝ → ℝ} {zset : Set ℝ}
    (hdef : zset = {x | (αleft ≤ x ∧ x ≤ αright) ∧ g x = 0}) (hg : Continuous g) :
    IsClosed zset := by
  subst zset
  apply IsClosed.inter
  · exact isClosed_Icc
  · change IsClosed (g ⁻¹' {0})
    apply IsClosed.preimage hg
    exact T1Space.t1 0

[haotian liu]

Thank you very much!