ext — Mathlib

English

The map from continuous alternating maps to alternating maps is injective: if f and g have the same alternating map, then f = g.

Русский

Обратная карта от непрерывных чередующихся отображений к чередующимся отображениям инъективна: если f и g имеют одинаковое чередующее отображение, то они равны.

LaTeX

$$$\\forall f,g : \\mathrm{ContinuousAlternatingMap}(R,M,N,\\iota),\\; f.toAlternatingMap = g.toAlternatingMap \\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {f g : M [⋀^ι]→L[R] N} (H : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ H

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