Zulip Chat Archive

Stream: general

Topic: Using a definition in statement of lemma

Quinn Culver (Jan 17 2023 at 04:19):

How do I correctly use collinear in triangle_non_degen ? Seems like since the type of collinear is Prop, it should work as I have it.

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

variables (P L)
structure triangle :=
(p₀ p₁ p₂ : P)
(l₀ l₁ l₂ : L)
(i₀₁ : p₀  l₁)
(i₀₂ : p₀  l₂)
(i₁₀ : p₁  l₀)
(i₁₂ : p₁  l₂)
(i₂₀ : p₂  l₀)
(i₂₁ : p₂  l₁)

variables {P}
def collinear (p₀ p₁ p₂ : P) : Prop :=  l : L, p₀  l  p₁  l  p₂  l

lemma triangle_non_degen (T : triangle P L) (i₀₀ : T.p₀  T.l₀) :  collinear (T.p₀ T.p₁ T.p₂) :=  sorry

Heather Macbeth (Jan 17 2023 at 04:23):

@Quinn Culver collinear L T.p₀ T.p₁ T.p₂ should do it.

Quinn Culver (Jan 17 2023 at 04:37):

Thanks @Heather Macbeth. Give Antonella a big hug for me! :hug:

Last updated: Aug 03 2023 at 10:10 UTC