mem_finsupport — Mathlib

English

i belongs to finsupport x0 iff i belongs to the support of the function i ↦ f_i(x0).

Русский

i ∈ finsupport x0 эквивалентно i ∈ опоре функции i ↦ f_i(x0).

LaTeX

$$$\forall x_0, \; i \in ρ.finsupport x_0 \iff i \in \operatorname{support}(\lambda i. ρ(i)(x_0))$$$

Lean4

@[simp]
theorem mem_finsupport (x₀ : X) {i} : i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i ↦ ρ i x₀ := by
  simp only [finsupport, mem_support, Finite.mem_toFinset, mem_setOf_eq]

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