Theorems · Definition · combinatorics

Configuration.ProjectivePlane.mk.noConfusion

{P : Type u_1} →
  {L : Type u_2} →
    {inst : Membership P L} →
      {P_1 : Sort u} →
        {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₃} →
                {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₃} →
                        { toHasPoints := toHasPoints, mkLine := mkLine, mkLine_ax := mkLine_ax,
                              exists_config := exists_config } =
                            { toHasPoints := toHasPoints', mkLine := mkLine', mkLine_ax := mkLine_ax',
                              exists_config := exists_config' } →
                          (toHasPoints ≍ toHasPoints' → mkLine ≍ mkLine' → P_1) → P_1

Defined in

Mathlib.Combinatorics.Configuration

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms