Theorems · Definition · combinatorics

Configuration.ProjectivePlane.casesOn

{P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      {motive : Configuration.ProjectivePlane P L → Sort u} →
        (t : Configuration.ProjectivePlane P L) →
          ([toHasPoints : Configuration.HasPoints P L] →
              (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
                (mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) →
                  (exists_config :
                      ∃ p₁ p₂ p₃ l₁ l₂ l₃,
                        p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃) →
                    motive
                      { toHasPoints := toHasPoints, mkLine := mkLine, mkLine_ax := mkLine_ax,
                        exists_config := exists_config }) →
            motive t

Defined in

Mathlib.Combinatorics.Configuration

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

Membership