symm_source — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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