comap_restrict — Mathlib

English

For t ⊆ u, the volume of the image of t under the subtype inclusion is bounded by the volume of t.

Русский

Для t ⊆ u объём образа t через включение подтипа ограничен объёмом t.

LaTeX

$$$\text{volume}(((↑) : u → δ) '' t) \le \text{volume}(t).$$$

Lean4

theorem comap_restrict (μ : Measure β) (s : Set β) : (μ.restrict s).comap f = (μ.comap f).restrict (f ⁻¹' s) :=
  by
  ext t ht
  rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf, Measure.restrict_apply (hf.measurableSet_image.2 ht),
    image_inter_preimage]

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