refl_restr_target — Mathlib

English

The identity partial equivalence on a set s is given by the identity map with source and target equal to s.

Русский

Тождественная частичная эквивалентность на множестве s задаётся тождественным отображением, источником и целью которых являются s.

LaTeX

$$$\\text{ofSet}(s): \\alpha \\simeq \\alpha$ with\\source = s, \\target = s$$$

Lean4

@[mfld_simps]
theorem refl_restr_target (s : Set α) : ((PartialEquiv.refl α).restr s).target = s := by simp

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