isSubordinate_toPartitionOfUnity — Mathlib

English

For a smooth partition of unity f with its underlying partition f.toPartitionOfUnity, the subordinate relation to U is equivalent whether we view f as a smooth partition of unity or as its underlying partition of unity.

Русский

Для гладкого разбиения единиц f и его базовой разбиения единиц f.toPartitionOfUnity отношение подчинённости к U эквивалентно в обоих представлениях.

LaTeX

$$$\operatorname{IsSubordinate}(f,U) \quad\text{iff}\quad \operatorname{IsSubordinate}(f^{\mathrm{PU}},U),$ где $f^{\mathrm{PU}}=f.toPartitionOfUnity$.$$

Lean4

@[simp]
theorem isSubordinate_toPartitionOfUnity : f.toPartitionOfUnity.IsSubordinate U ↔ f.IsSubordinate U :=
  Iff.rfl

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