Theorems · Theorem · general topology

BumpCovering.toPOUFun_eq_mul_prod

∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (i : ι) (x : X)
  (t : Finset ι),
  (∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t) →
    f.toPOUFun i x = (f i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (f j) x)

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace