Theorems · Theorem · order theory

Set.Finite.exists_lt_map_eq_of_forall_mem

∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] {t : Set β} {f : α → β} [Infinite α],
  (∀ (a : α), f a ∈ t) → t.Finite → ∃ a b, a < b ∧ f a = f b

Defined in

Mathlib.Order.Preorder.Finite

Cited by

6 results in Mathlib

Foundations

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

Assumes

LinearOrderInfinite