toPartialEquiv — Mathlib

English

If e.IsImage s t, then the corresponding partial equivalence preserves this image relation.

Русский

Если e.IsImage s t, то соответствующее частично эквивалентное отображение сохраняет это отношение образа.

LaTeX

$$$\\text{If } e.IsImage\\, s\\, t \\text{ then } e.toPartialEquiv.IsImage\\, s\\, t$$$

Lean4

theorem toPartialEquiv (h : e.IsImage s t) : e.toPartialEquiv.IsImage s t :=
  h

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