The set of zeros of a continuous function

Stream: mathlib4

[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?

private theorem has_minimal_zero {αleft αright : ℝ} {g : ℝ → ℝ} {zset : Set ℝ}
    (hdef : zset = {x | (αleft ≤ x ∧ x ≤ αright) ∧ g x = 0}) (h : Set.Nonempty zset) (hg : Continuous g) :
  ∃ a ∈ zset, ∀ b ∈ zset, a ≤ b := by
  sorry

[Yury G. Kudryashov]

See docs#IsClosed.csInf_mem or docs#IsCompact.exists_isLeast

[Josha Dekker]

Edit: I misread, ignore this message
g x = 0 in hdef is not necessary here, right? This is a compact function on a compact set, so we can use Weierstrass, which is the second link that Yury sent.

[Yury G. Kudryashov]

There is no g in the conclusion. We only need it to prove that zset is closed.

[haotian liu]

Thank you for your answer.
Is there any theorem in Lean that can help us to prove that the zset is a closed set?

[Josha Dekker]

Haotian Liu said:

Thank you for your answer.
Is there any theorem in Lean that can help us to prove that the zset is a closed set?

I can’t search them now, but all of the following steps should be in Mathlib:

Pre-image of a continuous function g of a closed set, {0}, is closed, which are all zeros of g. The interval (Icc aleft aright) is closed. The intersection of two closed sets is closed. This is exactly your proof.

[Yury G. Kudryashov]

BTW, I think that the #new members stream is a better place for questions like that.

[haotian liu]

OK, Thank you very much!