id — Mathlib · SciLib

English

The identity function as an element of C(s,R)₀ when 0 ∈ s is given by the restriction of the identity on R to s.

Русский

Идентичность на множестве s как элемент C(s,R)₀ задаётся ограничением тождественной функции на R к s.

LaTeX

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

Lean4

/-- The identity function as an element of `C(s, R)₀` when `0 ∈ (s : Set R)`. -/
@[simps!]
protected def id (s : Set R) [Fact (0 ∈ s)] : C(s, R)₀ :=
  ⟨.restrict s (.id R), rfl⟩

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