map_map

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.map_map

English

Mapping by g after f equals mapping by g ∘ f.

Русский

Отображение функций g после f эквивалентно отображению g ∘ f.

LaTeX

$$$ \text{map } g (\text{map } f \, l) = \text{map } (g \circ f) \, l $$$

Lean4

@[simp]
theorem map_map (g : β → γ) (f : α → β) (l : Language α) : map g (map f l) = map (g ∘ f) l := by simp [map, image_image]

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

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

Разделы

Аффилиация

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