volume_apply — Mathlib

English

For any subset s of I, the volume of s equals the volume of its image under the inclusion: volume s = volume (val '' s).

Русский

Для любого множества s ⊆ I объём равен объёму образа этого множества под вложением: volume s = volume (val '' s).

LaTeX

$$$\forall s \subseteq I:\, \operatorname{volume} s = \operatorname{volume} (\operatorname{Subtype.val} '' s)$$$

Lean4

theorem volume_apply {s : Set I} : volume s = volume (Subtype.val '' s) :=
  measurableEmbedding_coe.comap_apply ..

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