IsSubordinate — Mathlib

English

A partition of unity f is subordinate to a family U indexed by ι if for each i, tsupport(f_i) ⊆ U_i.

Русский

Разбиение единства f удовлетворяет условию подчинённости к семье U: для каждого i опора tsupport(f_i) ⊆ U_i.

LaTeX

$$IsSubordinate(U) := ∀ i, tsupport(f_i) ⊆ U(i)$$

Lean4

/-- A partition of unity `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 (U : ι → Set X) : Prop :=
  ∀ i, tsupport (f i) ⊆ U i

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