coe_sdiff — Mathlib

English

Let S and T be measurable subsets of α (i.e., elements of the subtype of measurable sets). Then the underlying set of their difference coincides with the set-theoretic difference of the underlying sets: the image of S \\ T equals S \\ T.

Русский

Пусть S и T будут измеримыми подмножествами α. Тогда порождение разности S \ T соответствует обыкновенной разности множеств: подмножество S \ T равно S \\ T.

LaTeX

$$$\\uparrow\\bigl(s \\ t\\bigr) = \\bigl(s : \\mathrm{Set} \\alpha\\bigr) \\setminus t$$$

Lean4

@[simp]
theorem coe_sdiff (s t : Subtype (MeasurableSet : Set α → Prop)) : ↑(s \ t) = (s : Set α) \ t :=
  rfl

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