mem_support_toFun — Mathlib

English

For a dependent finitely supported function f, the index i lies in its support exactly when the i-th coordinate is nonzero.

Русский

У зависимой функции с конечной поддержкой индекс i принадлежит её опоре тогда и только тогда, когда i-я координата не равна нулю.

LaTeX

$$$i \\in f.{\\mathrm{support}} \\iff f_i \\neq 0$$$

Lean4

@[simp]
theorem mem_support_toFun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ 0 :=
  by
  obtain ⟨f, s⟩ := f
  induction s using Trunc.induction_on with
  | _ s
  dsimp only [support, Trunc.lift_mk]
  rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']
  exact and_iff_right_of_imp (s.prop i).resolve_right

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