graphOn_union — Mathlib

English

For sets s and t in α and a function f: α → β, the graph of f on the union s ∪ t is the union of the graphs on s and on t.

Русский

Для множеств s, t ⊆ α и функции f: α → β граф функции f на объединении s ∪ t равен объединению графов на s и на t.

LaTeX

$$$\operatorname{graphOn}(f, s \cup t) = \operatorname{graphOn}(f,s) \cup \operatorname{graphOn}(f,t)$$$

Lean4

@[simp]
theorem graphOn_union (f : α → β) (s t : Set α) : graphOn f (s ∪ t) = graphOn f s ∪ graphOn f t :=
  image_union ..

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