map_id

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.map_id

English

Lifting the identity function yields the identity on germs.

Русский

Возведение тождественного отображения оставляет зародыши без изменений.

LaTeX

$$$ \mathrm{map}(\mathrm{id}) = \mathrm{id} $$$

Lean4

@[simp]
theorem map_id : map id = (id : Germ l β → Germ l β) := by
  ext ⟨f⟩
  rfl

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

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

Разделы

Аффилиация

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