Theorems · Theorem · combinatorics

Configuration.HasLines.exists_bijective_of_card_eq

∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [Configuration.HasLines P L] [inst_2 : Fintype P]
  [inst_3 : Fintype L],
  Fintype.card P = Fintype.card L →
    ∃ f, Function.Bijective f ∧ ∀ (l : L), Configuration.pointCount P l = Configuration.lineCount L (f l)

Defined in

Mathlib.Combinatorics.Configuration

Cited by

1 results in Mathlib

Foundations

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

Assumes

MembershipConfiguration.HasLinesFintypeFintype