Theorems · Theorem · combinatorics

Configuration.Nondegenerate.exists_injective_of_card_le

∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.Nondegenerate P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L], Fintype.card L ≤ Fintype.card P → ∃ f, Function.Injective f ∧ ∀ (l : L), f l ∉ l

If a nondegenerate configuration has at least as many points as lines, then there exists an injective function f from lines to points, such that f l does not lie on l.

Defined in

Mathlib.Combinatorics.Configuration

Cited by

2 results in Mathlib

Foundations

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

Assumes

MembershipConfiguration.NondegenerateFintypeFintype