map_le_restrict_range — Mathlib

English

For OuterMeasure ma, mb and map f, map f ma ≤ restrict (range f) mb iff map f ma ≤ mb.

Русский

Для внешней меры ma, mb и отображения f: map f ma ≤ restrict (range f) mb эквивалентно map f ma ≤ mb.

LaTeX

$$$map f ma \\le restrict (range f) mb \\iff map f ma \\le mb$$$

Lean4

@[simp]
theorem map_le_restrict_range {β} {ma : OuterMeasure α} {mb : OuterMeasure β} {f : α → β} :
    map f ma ≤ restrict (range f) mb ↔ map f ma ≤ mb :=
  ⟨fun h => h.trans (restrict_le_self _ _), fun h s => by simpa using h (s ∩ range f)⟩

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