IsSubordinate — Mathlib

English

A BumpCovering is subordinate to U iff every bump function is contained in its respective U_i.

Русский

BumpCovering подчинено U тогда и только тогда, когда каждая f_i имеет опору в U_i.

LaTeX

$$$$ f.IsSubordinate(U) \iff \forall i, \operatorname{tsupport}(f_i) \subseteq U_i. $$$$

Lean4

/-- 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`. -/
def IsSubordinate (f : BumpCovering ι X s) (U : ι → Set X) : Prop :=
  ∀ i, tsupport (f i) ⊆ U i

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