uliftDown — Mathlib

English

IsEmbedding (Sigma.map f1 f2) iff ∀ i, IsEmbedding (f2 i), assuming Injective f1.

Русский

Если f1 инъективен, то IsEmbedding (Sigma.map f1 f2) эквивалентно тому, что для каждого i отображение f2 i является вложением.

LaTeX

$$$ (h_1 : \operatorname{Injective}(f_1)) \Rightarrow \mathrm{IsEmbedding}(\mathrm{Sigma.map} f_1 f_2) \Leftrightarrow \forall i, \mathrm{IsEmbedding}(f_2 i).$$$

Lean4

theorem uliftDown [TopologicalSpace X] : IsEmbedding (ULift.down : ULift.{v, u} X → X) :=
  ⟨⟨rfl⟩, ULift.down_injective⟩

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