ext — Mathlib

English

Two measurable spaces on the same underlying set are equal if for every subset, the measurability predicates agree.

Русский

Два пространства измеримости на одной и той же основе равны, если для каждого подмножества совпадают признаки измеримости.

LaTeX

$$\forall m_1 m_2 : MeasurableSpace(\alpha), (\forall s : Set(\alpha), \mathrm{MeasurableSet}[m_1](s) \leftrightarrow \mathrm{MeasurableSet}[m_2](s)) \rightarrow m_1 = m_2$$

Lean4

@[ext]
theorem ext {m₁ m₂ : MeasurableSpace α} (h : ∀ s : Set α, MeasurableSet[m₁] s ↔ MeasurableSet[m₂] s) : m₁ = m₂ :=
  measurableSet_injective <| funext fun s => propext (h s)

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