graphOn_insert — Mathlib

English

For any s ⊆ α and x ∈ α, the graph of f on insert x s equals inserting the point (x, f(x)) into the graph on s.

Русский

Для любых s ⊆ α и x ∈ α граф f на вставке x в s равен вставке точки (x, f(x)) в граф на s.

LaTeX

$$$\operatorname{graphOn}(f, \operatorname{insert}(x,s)) = \operatorname{insert}( (x,f(x)) , \operatorname{graphOn}(f,s) )$$$

Lean4

@[simp]
theorem graphOn_insert (f : α → β) (x : α) (s : Set α) : graphOn f (insert x s) = insert (x, f x) (graphOn f s) :=
  image_insert_eq ..

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