apply_one_path — Mathlib

English

An abbreviation for constructing the product-to-product top transportation on lifted intervals.

Русский

Сокращённое обозначение для построения отображения от произведения к произведению на подъёме интервала.

LaTeX

$$$$ \\text{prodToProdTopI} \\;\\{a_1,a_2\\}\\;\\{b_1,b_2\\} = \\text{prodToProdTop}(TopCat.of\\; ULift I) \\; (X) $$$$

Lean4

/-- Proof that `g(p) = H(1 ⟶ 1, p)`, with the appropriate casts -/
theorem apply_one_path :
    (πₘ (TopCat.ofHom g)).map p =
      hcast (H.apply_one x₀).symm ≫
        (πₘ (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 1))) p) ≫
          hcast (H.apply_one x₁) :=
  Quotient.inductionOn p fun p' =>
    by
    apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
    intros
    rw [Path.prod_coe, ulift_apply H]
    simp

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