Theorems · Definition · general topology

BumpCovering.IsSubordinate

{ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → (ι → Set X) → Prop

A collection of bump functions f i is subordinate to a family of sets U i indexed by the same type if for each i the closure of the support of f i is a subset of U i.

Defined in

Mathlib.Topology.PartitionOfUnity

Cited by

15 results in Mathlib

Foundations

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

Assumes

TopologicalSpace