eventually_finsupport_subset

Mathlib.Topology.PartitionOfUnity

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

← MathLib Explorer

English

i ∈ finsupport x0 iff x0 ∈ tsupport f_i.

Русский

i ∈ finsupport x0 эквивалентно x0 ∈ tsupport f_i.

LaTeX

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

Lean4

theorem eventually_finsupport_subset : ∀ᶠ y in 𝓝 x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀ :=
  (ρ.eventually_fintsupport_subset x₀).mono fun y hy ↦ (ρ.finsupport_subset_fintsupport y).trans hy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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