extend — Mathlib

English

For a chart f on M, extend f by I to obtain a partial equivalence f.extend I, i.e., extend f by composing with I.

Русский

Для диаграммы f на M получить f.extend I, переход через I, т.е. расширение через композицию

LaTeX

$$extend : OpenPartialHomeomorph M H → PartialEquiv M E$$

Lean4

/-- Given a chart `f` on a manifold with corners, `f.extend I` is the extended chart to the model
vector space. -/
@[simp, mfld_simps]
def extend : PartialEquiv M E :=
  f.toPartialEquiv ≫ I.toPartialEquiv

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