ae_eq_trans

Mathlib.MeasureTheory.OuterMeasure.AE

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ae_eq_trans

English

If f =ᵐ[μ] g and g =ᵐ[μ] h, then f =ᵐ[μ] h.

Русский

Если f =ᵐ[μ] g и g =ᵐ[μ] h, то f =ᵐ[μ] h.

LaTeX

$$$(f =ᵐ[\\mu] g) \\land (g =ᵐ[\\mu] h) \\Rightarrow (f =ᵐ[\\mu] h)$$$

Lean4

theorem ae_eq_trans {f g h : α → β} (h₁ : f =ᵐ[μ] g) (h₂ : g =ᵐ[μ] h) : f =ᵐ[μ] h :=
  h₁.trans h₂

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

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

Разделы

Аффилиация

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