mem_range_of_measure_ne_zero — Mathlib

English

If the fiber of f over x has nonzero measure, then x lies in the range of f.

Русский

Если волокно f над x имеет ненулевую меру, то x принадлежит диапазону f.

LaTeX

$$$\\mu (f^{-1}({x})) \\neq 0 \\;\\Rightarrow\\; x \\in f.range$$$

Lean4

theorem mem_range_of_measure_ne_zero {f : α →ₛ β} {x : β} {μ : Measure α} (H : μ (f ⁻¹' { x }) ≠ 0) : x ∈ f.range :=
  let ⟨a, ha⟩ := nonempty_of_measure_ne_zero H
  mem_range.2 ⟨a, ha⟩

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