Theorems · Theorem · general topology

BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X),
  ∃ t, ⇑(f.toPartitionOfUnity i) =ᶠ[nhds x] ⇑(f i) * ⇑(∏ j ∈ t with WellOrderingRel j i, (1 - f j))

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

1 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace