range_toAlternatingMap — Mathlib

English

The map f is additive in any coordinate: f(m with i-th coordinate updated by x+y) equals f(m with i-th coordinate x) plus f(m with i-th coordinate y).

Русский

Отображение f линейно по каждой координате: если в i-й координате m обновить на x+y, то f равен сумме f при обновлении на x и на y.

LaTeX

$$$\\forall (m : ι \\to M) (i : ι) (x,y : M),\\; f(\\text{update } m\, i\, (x+y)) = f(\\text{update } m\, i\, x) + f(\\text{update } m\, i\, y)$$$

Lean4

@[simp]
theorem range_toAlternatingMap :
    Set.range (toAlternatingMap : M [⋀^ι]→L[R] N → (M [⋀^ι]→ₗ[R] N)) = {f : M [⋀^ι]→ₗ[R] N | Continuous f} :=
  Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.cont, fun h => ⟨{ f with cont := h }, DFunLike.ext' rfl⟩⟩

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