toContinuousMap_id — Mathlib

English

The map toContinuousMap of ContinuousMapZero.id s equals the restriction of the identity on R to s.

Русский

Отображение toContinuousMap для ContinuousMapZero.id s равно ограничению тождейности на R к s.

LaTeX

$$$\\operatorname{toContinuousMap}(\\text{ContinuousMapZero.id } s) = \\text{ContinuousMap.restrict } s (\\text{ContinuousMap.id } R)$$$

Lean4

@[simp]
theorem toContinuousMap_id {s : Set R} [Fact (0 ∈ s)] : (ContinuousMapZero.id s : C(s, R)) = .restrict s (.id R) :=
  rfl

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