mem_restrict_range — Mathlib

English

A restatement of mem_restrict_range showing the descriptive membership criterion for f.restrict s.

Русский

Переформулировка mem_restrict_range, задающая критерий принадлежности элемента диапазону f.restrict s.

LaTeX

$$$\\text{mem_restrict_range}$$$

Lean4

theorem mem_restrict_range {r : β} {s : Set α} {f : α →ₛ β} (hs : MeasurableSet s) :
    r ∈ (restrict f s).range ↔ r = 0 ∧ s ≠ univ ∨ r ∈ f '' s := by
  rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]

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