diff — Mathlib

English

Let e be a partial equivalence with e.IsImage s t and e.IsImage s' 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\\setminus s'\$\\(t\\setminus t')$$$

Lean4

protected theorem diff {s' t'} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s \ s') (t \ t') :=
  h.inter h'.compl

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