inducedMap_self — Mathlib

English

The induced map from β to β is the identity: for every b ∈ β, inducedMap β β b = b.

Русский

Индуцированное отображение β → β является тождественным: для всякого b ∈ β индуцированное отображение возвращает b.

LaTeX

$$$\\operatorname{inducedMap}_{\\beta,\\beta}(b) = b$$$

Lean4

@[simp]
theorem inducedMap_self (b : β) : inducedMap β β b = b :=
  eq_of_forall_rat_lt_iff_lt fun _ => coe_lt_inducedMap_iff

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