finite_tsupport — Mathlib

English

For any I with finsupport x0 ⊆ I, the sum over I of ρ_i(x0) equals 1.

Русский

Для любого I, содержащего finsupport x0, сумма по i∈I ρ_i(x0) равна 1.

LaTeX

$$$\forall x_0 ∈ s, \forall I, ρ.finsupport x_0 ⊆ I \Rightarrow \sum_{i ∈ I} ρ(i)(x_0) = 1$$$

Lean4

/-- The `tsupport`s of a partition of unity are locally finite. -/
theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite :=
  by
  rcases ρ.locallyFinite x₀ with ⟨t, t_in, ht⟩
  apply ht.subset
  rintro i hi
  simp only [inter_comm]
  exact mem_closure_iff_nhds.mp hi t t_in

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