target_eq — Mathlib

English

Two equivalent partial equivalences have the same target.

Русский

Две эквивалентные частичные эквивалентности имеют одинаковую область целевых значений.

LaTeX

$$$ e.target = e'.target $$$

Lean4

/-- Two equivalent partial equivs have the same target. -/
theorem target_eq {e e' : PartialEquiv α β} (h : e ≈ e') : e.target = e'.target := by
  simp only [← image_source_eq_target, ← source_eq h, h.2.image_eq]

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