connectedComponentsLift_apply_coe

English

For every x in α, the lifted value equals the original value, i.e., h.connectedComponentsLift(x) = f(x).

Русский

Для каждого элемента x из α приведенное значение лифта равно исходному значению: h.connectedComponentsLift(x) = f(x).

LaTeX

$$$\forall x \in \alpha:\; h.\text{connectedComponentsLift}(x) = f(x)$$$

Lean4

@[simp]
theorem connectedComponentsLift_apply_coe (h : Continuous f) (x : α) : h.connectedComponentsLift x = f x :=
  rfl

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