Theorems · Theorem · combinatorics

Configuration.HasLines.lineCount_eq_pointCount

∀ {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 →
    ∀ {p : P} {l : L}, p ∉ l → Configuration.lineCount L p = Configuration.pointCount P l

Defined in

Mathlib.Combinatorics.Configuration

Cited by

3 results in Mathlib

Foundations

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

Assumes

MembershipConfiguration.HasLinesFintypeFintype