Theorems · Definition · combinatorics

Finset.preimage

{α : Type u} → {β : Type v} → (s : Finset β) → (f : α → β) → Set.InjOn f (f ⁻¹' ↑s) → Finset α

Preimage of s : Finset β under a map f injective on f ⁻¹' s as a Finset.

Defined in

Mathlib.Data.Finset.Preimage

Cited by

108 results in Mathlib

Foundations

Depth 67 from the axioms, rests on 1,080 definitions · uses propext, Classical.choice, Quot.sound