measurableSet_injective — Mathlib

English

The map sending a measurable space to its family of measurable sets is injective; i.e., if two spaces have exactly the same measurable sets, they are equal.

Русский

Отображение, отправляющее пространство измеримости в множество измеримых подмножеств, инъективно; если два пространства имеют одинаковые множества, они равны.

LaTeX

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

Lean4

theorem measurableSet_injective : Injective (@MeasurableSet α)
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, _ => by congr

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