coe_inj

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

URI: https://scilib.ai/kg/mathlib#ContMDiffSection.coe_inj

English

Two sections are equal if their underlying pointwise values coincide for all x ∈ M.

Русский

Две секции равны тогда и только тогда, когда их значения в каждой точке совпадают.

LaTeX

$$$s=t \iff (\forall x, s(x)=t(x))$$$

Lean4

theorem coe_inj ⦃s t : Cₛ^n⟮I; F, V⟯⦄ (h : (s : ∀ x, V x) = t) : s = t :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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