Theorems · Theorem · order theory

Set.Finite.of_finite_fibers

∀ {α : Type u} {β : Type v} (f : α → β) {s : Set α}, (f '' s).Finite → (∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) → s.Finite

If the image of s under f is finite, and each fiber of f has a finite intersection with s, then s is itself finite. It is useful to give f explicitly here so this can be used with apply.

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound