forall_mem_range — Mathlib

English

If the measure of the preimage of a singleton under f is nonzero, then the value belongs to the range.

Русский

Если мера предобраза синглтона по f не ноль, то значение принадлежит диапазону.

LaTeX

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

Lean4

theorem forall_mem_range {f : α →ₛ β} {p : β → Prop} : (∀ y ∈ f.range, p y) ↔ ∀ x, p (f x) := by
  simp only [mem_range, Set.forall_mem_range]

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