ofMeasurableSpace_le_ofMeasurableSpace_iff

English

The field Has of a generated Dynkin system equals GenerateHas C, i.e., (generate C).Has = GenerateHas C, by definition.

Русский

Поле Has порожденной Dynkin-системы совпадает с GenerateHas C по определению.

LaTeX

$$$(\mathrm{generate} C).Has = \mathrm{GenerateHas} C$$$

Lean4

theorem ofMeasurableSpace_le_ofMeasurableSpace_iff {m₁ m₂ : MeasurableSpace α} :
    ofMeasurableSpace m₁ ≤ ofMeasurableSpace m₂ ↔ m₁ ≤ m₂ :=
  Iff.rfl

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