map_comm — Mathlib

English

If g1 ∘ f1 = g2 ∘ f2, then for every a, map g1 (map f1 a) = map g2 (map f2 a).

Русский

Если g1 ∘ f1 = g2 ∘ f2, то для каждого a выполняется map g1 (map f1 a) = map g2 (map f2 a).

LaTeX

$$$\text{If } g_1 \circ f_1 = g_2 \circ f_2, \text{ then } \forall a,\; \mathrm{WithBot.map}\ g_1 (\mathrm{WithBot.map}\ f_1\ a) = \mathrm{WithBot.map}\ g_2 (\mathrm{WithBot.map}\ f_2\ a)$$$

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 _

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