isSubordinate_toBumpCovering — Mathlib

English

For any x ∈ s, x lies in the source of the extChartAt chart at the index given by ind.

Русский

Для любого x ∈ s, x принадлежит области источника extChartAt для индекса ind.

LaTeX

$$$x \in s \land x ∈ ? ⇒ x \in (extChartAt I (fs.c (fs.ind x hx))).source$$$

Lean4

@[simp]
theorem isSubordinate_toBumpCovering {f : SmoothBumpCovering ι I M s} {U : M → Set M} :
    (f.toBumpCovering.IsSubordinate fun i => U (f.c i)) ↔ f.IsSubordinate U :=
  Iff.rfl

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