exists_pos_preimage_ball — Mathlib

English

For any f, x and nonzero μ, there exists n with μ(f^{-1}(Ball(x,n))) > 0.

Русский

Для любого отображения f, точки x и не нулевой меры μ существует n, такое что μ(f^{-1}(шар(x,n))) > 0.

LaTeX

$$$\exists n \in \mathbb{N}, μ(f^{-1}(\mathrm{Ball}(x,n))) > 0$$$

Lean4

theorem exists_pos_preimage_ball [PseudoMetricSpace δ] (f : α → δ) (x : δ) (hμ : μ ≠ 0) :
    ∃ n : ℕ, 0 < μ (f ⁻¹' Metric.ball x n) :=
  exists_pos_measure_of_cover (by rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]) hμ

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