map_id'

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.map_id'

English

If f is the identity on every element, then map f o = o.

Русский

Если f является тождественным отображением на каждом элементе, то map f o = o.

LaTeX

$$$ (\forall x, f x = x) \rightarrow \operatorname{map} f o = o $$$

Lean4

theorem map_id' {f : α → α} (H : ∀ x : α, f x = x) (o) : map f o = o := by rw [show f = id from funext H];
  exact id_map o

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru