constant_of_monotoneOn_antitoneOn

English

If f is monotone on a directed set s and antitone on s, then f is constant on s.

Русский

Если функция монотонна и антимонотонна на направленном множестве s, то она константна на s.

LaTeX

$$$\forall f\,s, MonotoneOn f s \to AntitoneOn f s \to DirectedOn (≤) s \to \forall a\in s, \forall b\in s, f(a)=f(b).$$$

Lean4

/-- If `f` is monotone and antitone on a directed set `s`, then `f` is constant on `s`. -/
theorem constant_of_monotoneOn_antitoneOn (hf : MonotoneOn f s) (hf' : AntitoneOn f s) (hs : DirectedOn (· ≤ ·) s) :
    ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → f a = f b := by
  rintro a ha b hb
  obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb
  exact le_antisymm ((hf ha hc hac).trans <| hf' hb hc hbc) ((hf hb hc hbc).trans <| hf' ha hc hac)

Похожие утверждения