union — Mathlib

English

If f maps every element of s1 into t and every element of s2 into t, then f maps every element of s1 ∪ s2 into t.

Русский

Если f переводит каждый элемент s1 в t и каждый элемент s2 в t, то f переводит каждый элемент s1 ∪ s2 в t.

LaTeX

$$$\\\\MapsTo f s_1 t \\\\land \\\\MapsTo f s_2 t \\\\rightarrow \\\\MapsTo f (s_1 \\\\cup s_2) t$$$

Lean4

theorem union (h₁ : MapsTo f s₁ t) (h₂ : MapsTo f s₂ t) : MapsTo f (s₁ ∪ s₂) t :=
  union_self t ▸ h₁.union_union h₂

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