union — Mathlib

English

Let e be a partial equivalence between α and β. If e maps s onto t and e maps s' onto t', then e maps s ∪ s' onto t ∪ t'.

Русский

Пусть e — частичное эквивалентство между α и β. Если e переводит s на t и одновременно переводит s' на t', то e переводит объединениеs ∪ s' на t ∪ t'.

LaTeX

$$$\\forall e:\\,\\mathrm{PartialEquiv}(\\alpha,\\beta),\\; s,t,s',t'\\subseteq \\alpha,\\beta,\\; h:\\ e.isImage\\,s\\,t,\\; h':\\ e.isImage\\,s'\\,t'\\Rightarrow e.isImage\\,(s\\cup s')\\,(t\\cup t')$$$

Lean4

protected theorem union {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∪ s') (t ∪ t') := fun _ hx =>
  or_congr (h hx) (h' hx)

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