Theorems · Inductive type · general topology

PartialEquiv

Type u_5 → Type u_6 → Type (max u_5 u_6)

Local equivalence between subsets source and target of α and β respectively. The (global) maps toFun : α → β and invFun : β → α map source to target and conversely, and are inverse to each other there. The values of toFun outside of source and of invFun outside of target are irrelevant.

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

335 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms