Theorems · Definition · logic and foundations

Set.RightInvOn

{α : Type u} → {β : Type v} → (β → α) → (α → β) → Set β → Prop

g is a right inverse to f on t if f (g x) = x for all x ∈ t.

Defined in

Mathlib.Data.Set.Operations

Cited by

47 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms