liftCover_coe' — Mathlib

English

For each s ∈ A, restricting LiftCover' to s yields F s hs: (liftCover' A F hF hA) restricted to s equals F s hs.

Русский

Для каждого s ∈ A ограничение LiftCover' до s даёт F s hs: (liftCover' A F hF hA) ограниченно до s равно F s hs.

LaTeX

$$$\\mathrm{restrict}\\ s\\ (\\mathrm{liftCover}'\\ A\\ F\\ hF\\ hA) = F\\,s\\,hs$$$

Lean4

@[simp]
theorem liftCover_coe' {s : Set α} {hs : s ∈ A} (x : s) : liftCover' A F hF hA x = F s hs x :=
  let x' : ((↑) : A → Set α) ⟨s, hs⟩ := x
  by delta liftCover'; exact ContinuousMap.liftCover_coe x'

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