trans

Mathlib.MeasureTheory.VectorMeasure.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans

← MathLib Explorer

English

For any v, v ≪ᵥ v holds.

Русский

Для любой v выполняется v ≪ᵥ v.

LaTeX

$$v ≪ᵥ v$$

Lean4

@[trans]
theorem trans {u : VectorMeasure α L} {v : VectorMeasure α M} {w : VectorMeasure α N} (huv : u ≪ᵥ v) (hvw : v ≪ᵥ w) :
    u ≪ᵥ w := fun _ hs => huv <| hvw hs

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru