refl_source — Mathlib

English

The identity partial equivalence on a set s has both its domain and codomain equal to s, with maps being the identity.

Русский

Частичное биективное отображение-идентичность на множества s имеет область определения и цель равные s, карты — тождественные.

LaTeX

$$$\text{forSet}(s) :\; \operatorname{source} = s,\; \operatorname{target} = s,\; \text{toFun} = \mathrm{id},\; \text{invFun} = \mathrm{id}$$$

Lean4

@[simp, mfld_simps]
theorem refl_source : (PartialEquiv.refl α).source = univ :=
  rfl

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