graphOn_comp — Mathlib

English

The graph of a composition g ∘ f on a set s is the image of the graphOn f on s under the map (a,b) ↦ (a, g(b)).

Русский

Граф на композиции g ∘ f над s равен образу графа f над s под отображением (a,b) ↦ (a, g(b)).

LaTeX

$$$\operatorname{graphOn}(g \circ f, s) = \{ (a, g(b)) : (a,b) \in \operatorname{graphOn}(f,s) \}$$$

Lean4

theorem graphOn_comp (s : Set α) (f : α → β) (g : β → γ) : s.graphOn (g ∘ f) = (fun x ↦ (x.1, g x.2)) '' s.graphOn f :=
  by simpa using image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _

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