eq_liftPath_iff' — Mathlib

English

A stronger variant: equality of lifts is equivalent to equality of their compositions with p and the initial point equality.

Русский

Усиленный вариант: равенство подъёмов эквивалентно равенству их композиции с p и начальному условию.

LaTeX

$$$$\Gamma = cov.liftPath(\gamma,e,\gamma_0) \iff p \circ \Gamma = \gamma \land \Gamma(0)=e.$$$$

Lean4

/-- Unique characterization of the lifted path. -/
theorem eq_liftPath_iff' {Γ : C(I, E)} : Γ = cov.liftPath γ e γ_0 ↔ p ∘ Γ = γ ∧ Γ 0 = e := by
  simp_rw [← DFunLike.coe_fn_eq, eq_liftPath_iff, and_iff_right (ContinuousMap.continuous _)]

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