mem_fintsupport_iff

Mathlib.Geometry.Manifold.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#SmoothPartitionOfUnity.mem_fintsupport_iff

English

For any i, i ∈ finsupport x0 iff i ∈ tsupport (ρ i x0).

Русский

Для любого i, i ∈ finsupport x0 тогда и только тогда, когда i ∈ tsupport (ρ i x0).

LaTeX

$$$i \in ρ.finsupport x_0 \iff i \in tsupport (ρ i x_0)$$$

Lean4

theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport (ρ i) :=
  Finite.mem_toFinset _

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

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

Разделы

Аффилиация

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