def ProjectivePair.tubesThrough {P : Type u_1} {T : Type u_2} (mem : P → T → Prop) (𝕋 : Set T) (x : P) : Set T

The set of tubes from a collection 𝕋 that pass through a given point x, where membership is given by an abstract relation mem : P → T → Prop.

def ProjectivePair.tubeDirections {T : Type u_2} {D : Type u_3} (dir : T → D) (S : Set T) : Set D

The set of directions of a family of tubes S ⊆ T, where each tube t : T has a direction dir t : D.

def ProjectivePair.IsProjective {P : Type u_1} {T : Type u_2} {D : Type u_3} (mem : P → T → Prop) (dir : T → D) (E : Set P) (𝕋 : Set T) : Prop

A pair (E, 𝕋) of points and tubes is projective if the set of directions of tubes through x₁ and through x₂ agree, for all x₁, x₂ ∈ E. Equivalently, every point of E "sees" the same directions of tubes from 𝕋.