support_intCast — Mathlib

English

For an additive group β with CharZero, and an integer n ≠ 0, the support of the function n : α → β is all of α (univ).

Русский

Для β с CharZero и целого n ≠ 0 множество поддержки константной функции n: α → β равно всему α (univ).

LaTeX

$$$\\text{support}(n:\\alpha\\to\\beta)=\\text{univ}$, если $n\\neq0$$$

Lean4

theorem support_intCast (hn : n ≠ 0) : support (n : α → β) = univ :=
  support_const <| Int.cast_ne_zero.2 hn

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