coe_finsupport

Mathlib.Topology.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#PartitionOfUnity.coe_finsupport

English

The finsupport x0, viewed as a set, equals the support of the function i ↦ f_i(x0).

Русский

Finsupport x0 как множество совпадает с опорой функции i ↦ f_i(x0).

LaTeX

$$$ρ.finsupport x_0 = \operatorname{support}(i \mapsto ρ(i)(x_0))$$$

Lean4

@[simp]
theorem coe_finsupport (x₀ : X) : (ρ.finsupport x₀ : Set ι) = support fun i ↦ ρ i x₀ :=
  by
  ext
  rw [Finset.mem_coe, mem_finsupport]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru