measurableEmbedding_sigmoid_comp_embeddingReal

English

For any type α with a measurable space and standard Borel, the composition of the sigmoid with the standard embedding from α is a measurable embedding.

Русский

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

LaTeX

$$$\operatorname{MeasurableEmbedding}(\operatorname{unitInterval.sigmoid} \circ \operatorname{MeasureTheory.embeddingReal}(\alpha))$$$

Lean4

theorem measurableEmbedding_sigmoid_comp_embeddingReal :
    MeasurableEmbedding (unitInterval.sigmoid ∘ MeasureTheory.embeddingReal α) :=
  measurableEmbedding_sigmoid.comp (MeasureTheory.measurableEmbedding_embeddingReal α)

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