continuousOn — Mathlib

English

Composition of a trivialization with a homeomorphism gives a new trivialization with composed projection.

Русский

Сочетание тривиализации с гомеоморфизмом задаёт новую тривиализацию с композиционной проекцией.

LaTeX

$$$ (e \text{.compHomeomorph} \ h) : Trivialization F (proj \circ h) $$$

Lean4

protected theorem continuousOn : ContinuousOn e' e'.source :=
  e'.continuousOn_toFun

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