Theorems · Definition · combinatorics

Configuration.HasLines.recOn

{P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      {motive : Configuration.HasLines P L → Sort u} →
        (t : Configuration.HasLines P L) →
          ([toNondegenerate : Configuration.Nondegenerate P L] →
              (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
                (mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) →
                  motive { toNondegenerate := toNondegenerate, mkLine := mkLine, mkLine_ax := mkLine_ax }) →
            motive t

Defined in

Mathlib.Combinatorics.Configuration

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

Membership