eq_liftHomotopy_iff' — Mathlib

English

A variant stating that equality of H' with liftHomotopy is equivalent to pointwise conditions on H' and H.

Русский

Вариант утверждения, что равенство H' и подъёма по гомотопии эквивалентно покомпонентному условию на H' и H.

LaTeX

$$$$H' = cov.liftHomotopy(H,f,H_0) \iff p \circ H' = H \land \forall a, H'(0,a) = f(a).$$$$

Lean4

theorem eq_liftHomotopy_iff' (H' : C(I × A, E)) : H' = cov.liftHomotopy H f H_0 ↔ p ∘ H' = H ∧ ∀ a, H' (0, a) = f a :=
  by
  simp_rw [← DFunLike.coe_fn_eq, eq_liftHomotopy_iff]
  exact and_iff_right fun a ↦ H'.2.comp (.prodMk_left a)

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