countable_setOf_two_preimages — Mathlib

English

If f is monotone on α→β, then there are at most countably many values c with two preimages.

Русский

Если f монотонна в направлении α→β, то существует не более счетного числа значений c, которые достигаются двумя разными аргументами.

LaTeX

$$$\text{Monotone } f \rightarrow \text{Set.Countable}\{c \mid \exists x

Lean4

/-- If a function is monotone in a second countable topological space, then there
are only countably many points that have several preimages. -/
theorem countable_setOf_two_preimages [SecondCountableTopology α] (hf : Monotone f) :
    Set.Countable {c | ∃ x y, x < y ∧ f x = c ∧ f y = c} :=
  by
  rw [← monotoneOn_univ] at hf
  simpa using hf.countable_setOf_two_preimages

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