English
Given a measurable space m on α, a predicate p, and a proof that p s ↔ MeasurableSet[m] s for all s, the copy defines a new measurable space on α with MeasurableSet' = p.
Русский
Для пространства измеримости m на α и предиката p, если для каждого s выполняется p s ↔ MeasurableSet[m] s, то копия задаёт новое пространство измеримости на α с MeasurableSet' = p.
LaTeX
$$$\text{copy}(m,p,h) \text{ is a MeasurableSpace on } \alpha$ with MeasurableSet' = p$$
Lean4
/-- Copy of a `MeasurableSpace` with a new `MeasurableSet` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (m : MeasurableSpace α) (p : Set α → Prop) (h : ∀ s, p s ↔ MeasurableSet[m] s) : MeasurableSpace α
where
MeasurableSet' := p
measurableSet_empty := by simpa only [h] using m.measurableSet_empty
measurableSet_compl := by simpa only [h] using m.measurableSet_compl
measurableSet_iUnion := by simpa only [h] using m.measurableSet_iUnion
