English
Mapping twice composes: Map (Map r f1 g1) f2 g2 = Map r (f2 ∘ f1) (g2 ∘ g1).
Русский
Два последовательных отображения составляются: Map (Map r f1 g1) f2 g2 = Map r (f2 ∘ f1) (g2 ∘ g1).
LaTeX
$$$\forall r:\alpha\to\beta\to \mathrm{Prop}\; (f1:\alpha\to\gamma)\,(g1:\beta\to\delta)\,(f2:\gamma\to\varepsilon)\,(g2:\delta\to\zeta),\; \mathrm{Map}(\mathrm{Map}(r,f1,g1),f2,g2) = \mathrm{Map}(r,(f2\circ f1),(g2\circ g1))$$$
Lean4
@[simp]
theorem map_map (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) :
Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) := by grind [Relation.Map]
