map_comm

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.map_comm

← MathLib Explorer

English

If f is injective, then map f is injective on WithTop.

Русский

Если f инъективен, то map f инъективен на WithTop.

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\text{Injective}(\\mathrm{WithTop.map}\\, f)$$$

Lean4

theorem map_comm {f₁ : α → β} {f₂ : α → γ} {g₁ : β → δ} {g₂ : γ → δ} (h : g₁ ∘ f₁ = g₂ ∘ f₂) (a : α) :
    map g₁ (map f₁ a) = map g₂ (map f₂ a) :=
  Option.map_comm h _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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