A nonzero function does not change sign

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Do we have sth like this in Mathlib?

import Mathlib

lemma constant_sign {f : ℝ → ℝ} {s : Set ℝ} (hs : IsPreconnected s) (hf : ContinuousOn f s)
    (hfx : ∀ x ∈ s, f x ≠ 0) : f '' s ⊆ Set.Ioi 0 ∨ f '' s ⊆ Set.Iio 0 :=
  (hs.image f hf).subset_or_subset isOpen_Ioi isOpen_Iio (by grind)
  (by grind : f '' s ⊆ Set.Ioi 0 ∪ Set.Iio 0)

lemma constant_sign' {f : ℝ → ℝ} {s : Set ℝ} (hs : IsPreconnected s) (hf : ContinuousOn f s)
    (hfx : ∀ x ∈ s, f x ≠ 0) : (∀ x ∈ s, 0 < f x) ∨ ∀ x ∈ s, f x < 0 := by
  rcases constant_sign hs hf hfx with (ha | hb)
  · exact Or.inl fun x hx => by simp_all; grind
  · exact Or.inr fun x hx => by simp_all; grind

If not, does it make sense to make a PR for this? I think one use this lemma quite often, but the proof is somewhat short.

[Notification Bot]

This topic was moved here from #Is there code for X? > A nonzero function do not change sign by Yongxi Lin (Aaron).

[Violeta Hernández]

This should be generalized from 0 to an arbitrary real, but otherwise I don't see a reason not to have it.

[Joseph Myers]

Also, arbitrary domain, and arbitrary LinearOrder OrderTopology codomain, I think.

[Michael Rothgang]

I have wanted such a result in the past (e.g., in #16553) --- this would be great to have, in the appropriate generality!

[Yongxi Lin (Aaron)]

#34596

[Yongxi Lin (Aaron)]

Michael Rothgang said:

I have wanted such a result in the past (e.g., in #16553) --- this would be great to have, in the appropriate generality!

Orientation of manifolds is exactly the kind of application I had in mind for this lemma!