structure ProjectionIncidence.Line2 : Type

A line in ℝ², encoded as a nonempty affine subspace of dimension 1.

• carrier : AffineSubspace ℝ (Fin 2 → ℝ)
• dim_eq : Module.finrank ℝ ↥self.carrier.direction = 1
• nonempty : (↑self.carrier).Nonempty

@[implicit_reducible]

instance ProjectionIncidence.instMembershipForallFinOfNatNatRealLine2 : Membership (Fin 2 → ℝ) Line2

A point p ∈ ℝ² belongs to a line l : Line2 iff it lies in the underlying affine subspace.

noncomputable def ProjectionIncidence.incidenceCount (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) : ℕ

The number of incidences I(X, L) = #{(x, ℓ) ∈ X × L : x ∈ ℓ} between a finite set of points X ⊆ ℝ² and a finite set of lines L.