English
In a second-countable space, under a certain nontrivial mapping, there exist a and b with a ≠ b such that both neighborhoods have positive μ-preimage measure.
Русский
В пространстве второй счётности существует точки a и b, разные, такие что любая окрестность a и окрестность b имеют положительную меру прообраза.
LaTeX
$$$\exists a,b\ (a\neq b)\ \wedge\ (∀ s\in \mathcal{N}(a), μ(f^{-1}(s))>0) \wedge (∀ t\in \mathcal{N}(b), μ(f^{-1}(t))>0)$$$
Lean4
/-- If a set has zero measure in a neighborhood of each of its points, then it has zero measure
in a second-countable space. -/
theorem exists_ne_forall_mem_nhds_pos_measure_preimage {β} [TopologicalSpace β] [T1Space β] [SecondCountableTopology β]
[Nonempty β] {f : α → β} (h : ∀ b, ∃ᵐ x ∂μ, f x ≠ b) :
∃ a b : β, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t) := by
-- We use an `OuterMeasure` so that the proof works without `Measurable f`
set m : OuterMeasure β := OuterMeasure.map f μ.toOuterMeasure
replace h : ∀ b : β, m { b }ᶜ ≠ 0 := fun b => not_eventually.mpr (h b)
inhabit β
have : m univ ≠ 0 := ne_bot_of_le_ne_bot (h default) (measure_mono <| subset_univ _)
rcases exists_mem_forall_mem_nhdsWithin_pos_measure this with ⟨b, -, hb⟩
simp only [nhdsWithin_univ] at hb
rcases exists_mem_forall_mem_nhdsWithin_pos_measure (h b) with ⟨a, hab : a ≠ b, ha⟩
simp only [isOpen_compl_singleton.nhdsWithin_eq hab] at ha
exact ⟨a, b, hab, ha, hb⟩
