countable_setOf_two_preimages — Mathlib

English

If a function is monotone on a set in a second countable space, the set of values c with two preimages is countable.

Русский

Если функция монотонна на множестве в пространстве второй счетности, тогда множество значений c, для которых найдутся два разных аргумента с одинаковым значением, счетно.

LaTeX

$$$\text{MonotoneOn}\ f\ s \rightarrow \text{Set.Countable}\{c \mid \exists x,y \in s, x

Lean4

/-- If a function is monotone on a set in a second countable topological space, then there
are only countably many points that have several preimages. -/
theorem countable_setOf_two_preimages [SecondCountableTopology α] (hf : MonotoneOn f s) :
    Set.Countable {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c} :=
  by
  nontriviality α
  let t := {c | ∃ x, ∃ y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
  have : ∀ c ∈ t, ∃ x, ∃ y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c := fun c hc ↦ hc
  choose! x y hxs hys hxy hfx hfy using this
  let u := x '' t
  suffices H : Set.Countable (x '' t)
    by
    have : Set.InjOn x t := by
      intro c hc d hd hcd
      have : f (x c) = f (x d) := by simp [hcd]
      rwa [hfx _ hc, hfx _ hd] at this
    exact countable_of_injective_of_countable_image this H
  apply Set.PairwiseDisjoint.countable_of_Ioo (y := fun a ↦ y (f a)); swap
  · rintro a ⟨c, hc, rfl⟩
    rw [hfx _ hc]
    exact hxy _ hc
  simp only [PairwiseDisjoint, Set.Pairwise, mem_image, onFun, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro c hc d hd hcd
  wlog H : c < d generalizing c d with h
  · apply (h d hd c hc hcd.symm ?_).symm
    have : c ≠ d := fun h ↦ hcd (congrArg x h)
    order
  simp only [disjoint_iff_forall_ne, mem_Ioo, ne_eq, and_imp]
  rintro a xca ayc b xda ayd rfl
  rw [hfx _ hc] at ayc
  have : x d ≤ y c := (xda.trans ayc).le
  have : f (x d) ≤ f (y c) := hf (hxs _ hd) (hys _ hc) this
  rw [hfx _ hd, hfy _ hc] at this
  exact not_le.2 H this

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