preimageHomeomorph_apply — Mathlib

English

For hb ⊆ e.baseSet and p in the preimage, the image under the preimageHomeomorph is the pair consisting of proj p and the fiber component of e p.

Русский

Для hb ⊆ e.baseSet и p ∈ proj^{-1}(s) величина e.preimageHomeomorph hb p равна паре ⟨proj p, (e p).2⟩.

LaTeX

$$$ e.preimageHomeomorph hb p = (\langle proj p, p.2 \rangle, (e p).2) $$$

Lean4

@[simp]
theorem preimageHomeomorph_apply {s : Set B} (hb : s ⊆ e.baseSet) (p : proj ⁻¹' s) :
    e.preimageHomeomorph hb p = (⟨proj p, p.2⟩, (e p).2) :=
  Prod.ext (Subtype.ext (e.proj_toFun p (e.mem_source.mpr (hb p.2)))) rfl

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