sourceHomeomorphBaseSetProd_apply

English

Evaluating the base product on an element of the source yields the pair formed by the base projection and fiber component.

Русский

При вычислении на элементе источника получаем пару (proj, fiber).

LaTeX

$$$ e.sourceHomeomorphBaseSetProd p = (\langle proj p, e.mem_source.mp p.2 \rangle, (e p).2) $$$

Lean4

@[simp]
theorem sourceHomeomorphBaseSetProd_apply (p : e.source) :
    e.sourceHomeomorphBaseSetProd p = (⟨proj p, e.mem_source.mp p.2⟩, (e p).2) :=
  e.preimageHomeomorph_apply subset_rfl ⟨p, e.mem_source.mp p.2⟩

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