liftCover_coe — Mathlib

English

On each piece S_i, the glued map agrees with the corresponding local map φ_i: for x ∈ S_i, (liftCover S φ hφ hS)(x) = φ_i(x).

Русский

На каждом фрагменте S_i склеенное отображение совпадает с соответствующим локальным отображением φ_i: для x ∈ S_i выполняется (liftCover S φ hφ hS)(x) = φ_i(x).

LaTeX

$$$\\forall i\\; \\forall x \\in S_i:\\ \\mathrm{liftCover}\\, S\\, φ\\, hφ\\, hS\\ x = φ_i(x)$$$

Lean4

@[simp]
theorem liftCover_coe {i : ι} (x : S i) : liftCover S φ hφ hS x = φ i x := by
  rw [liftCover, coe_mk, Set.liftCover_coe _]

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