le_def — Mathlib

English

For any two measurable spaces a and b on the same type, a ≤ b if and only if the collection of sets measurable in a is contained in the collection of sets measurable in b.

Русский

Для двух пространств измеримости a и b на одном и том же типе выполняется: a ≤ b тогда и только тогда, когда множество измеримых множеств a содержится в множестве измеримых множеств b.

LaTeX

$$$a \\le b \\iff a.MeasurableSet' \\le b.MeasurableSet'$$$

Lean4

theorem le_def {α} {a b : MeasurableSpace α} : a ≤ b ↔ a.MeasurableSet' ≤ b.MeasurableSet' :=
  Iff.rfl

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