div_toGerm

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.div_toGerm

English

The division operation on AEEqFun respects the germ construction: the germ of f/g equals the germ of f divided by the germ of g.

Русский

Операция деления на AEEqFun совместима с переходом к Germ: Germ(f/g) = Germ(f) / Germ(g).

LaTeX

$$$(f / g).toGerm = f.toGerm / g.toGerm$$$

Lean4

@[to_additive]
theorem div_toGerm (f g : α →ₘ[μ] γ) : (f / g).toGerm = f.toGerm / g.toGerm :=
  comp₂_toGerm _ _ _ _

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

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

Разделы

Аффилиация

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