Theorems · Definition · logic and foundations

Set.LeftInvOn

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

g is a left inverse to f on s means that g (f x) = x for all x ∈ s.

Defined in

Mathlib.Data.Set.Operations

Cited by

42 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms