toBumpCovering — Mathlib

English

The equivalence between IsSubordinate for SmoothBumpCovering and for their toBumpCovering is simp.

Русский

Эквивалентность подчинённости для SmoothBumpCovering и соответствующего BumpCovering тривиальна.

LaTeX

$$theorem isSubordinate_toBumpCovering {f} : (f.toBumpCovering.IsSubordinate (λ i, U (f.c i))) ↔ f.IsSubordinate U$$

Lean4

/-- Reinterpret a `SmoothBumpCovering` as a continuous `BumpCovering`. Note that not every
`f : BumpCovering ι M s` with smooth functions `f i` is a `SmoothBumpCovering`. -/
def toBumpCovering : BumpCovering ι M s
    where
  toFun i := ⟨fs i, (fs i).continuous⟩
  locallyFinite' := fs.locallyFinite
  nonneg' i _ := (fs i).nonneg
  le_one' i _ := (fs i).le_one
  eventuallyEq_one' := fs.eventuallyEq_one'

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