toGerm_injective

Mathlib.MeasureTheory.Function.AEEqFun

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

← MathLib Explorer

English

The map f ↦ f.toGerm from AEEqFun to germs is injective.

Русский

Отображение f ↦ f.toGerm инъективно.

LaTeX

$$$toGerm\_injective: \mathrm{Injective}(toGerm)$$$

Lean4

theorem toGerm_injective : Injective (toGerm : (α →ₘ[μ] β) → Germ (ae μ) β) := fun f g H =>
  ext <| Germ.coe_eq.1 <| by rwa [← toGerm_eq, ← toGerm_eq]

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

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

Разделы

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

Аффилиация

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