symm_target — Mathlib

English

The target of the inverse partial equivalence equals the source of the original partial equivalence: target(e.symm) = source(e).

Русский

Область значения обратного частичного эквив равна области определения исходного: target(e.symm) = source(e).

LaTeX

$$\mathrm{target}(e^{\mathrm{symm}}) = \mathrm{source}(e)$$

Lean4

@[simp, mfld_simps]
theorem symm_target : e.symm.target = e.source :=
  rfl

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