mk_injective

Mathlib.Data.Bundle

URI: https://scilib.ai/kg/mathlib#Bundle.TotalSpace.mk_injective

English

For a fixed base element b, the map y ↦ ⟨b, y⟩ is injective.

Русский

Для фиксированного b отображение y ↦ ⟨b, y⟩ инъективно.

LaTeX

$$$$\forall b,\ Injective(\lambda y:\, E(b) \mapsto \langle b, y\rangle).$$$$

Lean4

theorem mk_injective (b : B) : Injective (mk b : E b → TotalSpace F E) := fun _ _ ↦ mk_inj.1

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

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

Разделы

Аффилиация

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