copy_eq — Mathlib

English

Let (α, M) be a measurable space and p a predicate on subsets of α such that p(s) holds if and only if s is measurable with respect to M. Then the copy of M defined by p is equal to M.

Русский

Пусть (α, M) — пространство измеримости, и p — предикат над подмножествами α, удовлетворяющий p(s) ⇔ s измеримо относительно M. Тогда копия пространства, заданная p, равна M.

LaTeX

$$$\\forall \\alpha \\; \\forall m : MeasurableSpace\\,\\alpha \\; \\forall p : Set\\alpha \\to Prop \\; \\forall h : \\forall s, p\\,s \\leftrightarrow MeasurableSet[m]\\,s,\\; m.copy\\,p\\,h = m$$$

Lean4

theorem copy_eq {m : MeasurableSpace α} {p : Set α → Prop} (h : ∀ s, p s ↔ MeasurableSet[m] s) : m.copy p h = m :=
  ext h

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