mem_support — Mathlib

English

For any a in Γ, a is in the support of x if and only if the a-th coefficient of x is nonzero.

Русский

Для любого a ∈ Γ множество a принадлежит опоре x тогда и только тогда, когда коэффициент x при a не равен нулю.

LaTeX

$$$a \\in x.support \\iff x_{a} \\neq 0$$$

Lean4

@[simp]
theorem mem_support (x : HahnSeries Γ R) (a : Γ) : a ∈ x.support ↔ x.coeff a ≠ 0 :=
  Iff.refl _

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