def Line (α : Type u_2) [Ring α] : Type u_2

Equations

• Line α = { x : Submodule α (α × α × α) // FiniteDimensional.finrank α ↥x = 2 }

instance instSetLike {α : Type u_1} [Field α] : SetLike (Line α) (α × α × α)

Equations

• instSetLike = { coe := fun (x : Line α) => ↑↑x, coe_injective' := ⋯ }

theorem set_like_val {α : Type u_1} [Field α] {x : α × α × α} {l : Line α} : x ∈ l ↔ x ∈ ↑l

@[simp]

theorem Line_finrank {α : Type u_1} [Field α] {l : Line α} : FiniteDimensional.finrank α ↥↑l = 2

instance mem2 {α : Type u_1} [Field α] : Membership (α × α) (Line α)

Equations

• mem2 = { mem := fun (x : α × α) (l : Line α) => (x.1, x.2, 1) ∈ l }

noncomputable instance instDecidableMem2 {α : Type u_1} [Field α] (x : α × α) (y : Line α) : Decidable (x ∈ y)

Equations

• instDecidableMem2 x y = inferInstance

noncomputable instance instDecidableEqLine {α : Type u_1} [Field α] : DecidableEq (Line α)

Equations

• instDecidableEqLine = inferInstance

def Line.apply {α : Type u_1} [Field α] (l : Line α) (p : (α × α × α) ≃ₗ[α] α × α × α) : Line α

Equations

• Line.apply l p = { val := Submodule.map ↑p ↑l, property := ⋯ }

def apply_injective {α : Type u_1} [Field α] (l₁ : Line α) (l₂ : Line α) (p : (α × α × α) ≃ₗ[α] α × α × α) (h : Line.apply l₁ p = Line.apply l₂ p) : l₁ = l₂

Equations

• ⋯ = ⋯

instance mem3 {α : Type u_1} [Field α] : Membership (α × α) (Submodule α (α × α × α))

Equations

• mem3 = { mem := fun (x : α × α) (l : Submodule α (α × α × α)) => (x.1, x.2, 1) ∈ l }

theorem mem_iff_mem_val {α : Type u_1} [Field α] (x : α × α) (l : Line α) : x ∈ l ↔ x ∈ ↑l

def Submodule.pair {α : Type u_1} [Field α] (i : α × α) (j : α × α) : Submodule α (α × α × α)

Equations

• Submodule.pair i j = Submodule.span α {(i.1, i.2, 1), (j.1, j.2, 1)}

theorem mem_span1 {α : Type u_1} [Field α] (i : α × α) (j : α × α) : i ∈ Submodule.pair i j

theorem mem_span2 {α : Type u_1} [Field α] (i : α × α) (j : α × α) : j ∈ Submodule.pair i j

noncomputable def Submodule.pair_basis {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : Basis (Fin 2) α ↥(Submodule.pair i j)

Equations

• Submodule.pair_basis i j h = let_fun this := Basis.span ⋯; Basis.map this (LinearEquiv.ofEq (Submodule.span α (Set.range ![(i.1, i.2, 1), (j.1, j.2, 1)])) (Submodule.pair i j) ⋯)

theorem repr_pair_basis_first' {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : (Submodule.pair_basis i j h) 0 = { val := (i.1, i.2, 1), property := ⋯ }

theorem repr_pair_basis_first {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : (Submodule.pair_basis i j h).repr { val := (i.1, i.2, 1), property := ⋯ } = Finsupp.single 0 1

theorem repr_pair_basis_second' {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : (Submodule.pair_basis i j h) 1 = { val := (j.1, j.2, 1), property := ⋯ }

theorem repr_pair_basis_second {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : (Submodule.pair_basis i j h).repr { val := (j.1, j.2, 1), property := ⋯ } = Finsupp.single 1 1

def Line.of {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : Line α

Equations

• Line.of i j h = { val := Submodule.pair i j, property := ⋯ }

def Submodule.infinity (α : Type u_2) [Field α] : Submodule α (α × α × α)

Equations

• Submodule.infinity α = Submodule.span α {(1, 0, 0), (0, 1, 0)}

noncomputable def Submodule.infinity_basis (α : Type u_2) [Field α] : Basis (Fin 2) α ↥(Submodule.infinity α)

Equations

• Submodule.infinity_basis α = let_fun this := Basis.span ⋯; Basis.map this (LinearEquiv.ofEq (Submodule.span α (Set.range ![(1, 0, 0), (0, 1, 0)])) (Submodule.infinity α) ⋯)

theorem infinity_mem {α : Type u_1} [Field α] (x : α × α × α) : x ∈ ↑(Submodule.infinity α) ↔ x.2.2 = 0

theorem infinity_mem_first {α : Type u_1} [Field α] : (1, 0, 0) ∈ ↑(Submodule.infinity α)

theorem infinity_first {α : Type u_1} [Field α] : (Submodule.infinity_basis α) 0 = { val := (1, 0, 0), property := ⋯ }

theorem infinity_mem_second {α : Type u_1} [Field α] : (0, 1, 0) ∈ ↑(Submodule.infinity α)

theorem infinity_second {α : Type u_1} [Field α] : (Submodule.infinity_basis α) 1 = { val := (0, 1, 0), property := ⋯ }

def Line.infinity (α : Type u_2) [Field α] : Line α

Equations

• Line.infinity α = { val := Submodule.infinity α, property := ⋯ }

def Vnorm {α : Type u_1} [Field α] (x : α × α × α) : α × α

Equations

• Vnorm x = (x.1 / x.2.2, x.2.1 / x.2.2)

theorem norm_mem {α : Type u_1} [Field α] (l : Line α) (x : α × α × α) (h₂ : x.2.2 ≠ 0) : x ∈ ↑l ↔ Vnorm x ∈ l

theorem vnorm_eq_vnorm {α : Type u_1} [Field α] (x : α × α × α) (y : α × α × α) (h : Vnorm x = Vnorm y) (h₂ : x.2.2 ≠ 0) (h₃ : y.2.2 ≠ 0) : ∃ (r : α), r • x = y

theorem mem_line1 {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : i ∈ Line.of i j h

theorem mem_line2 {α : Type u_1} [Field α] (i : α × α) (j : α × α) (h : i ≠ j) : j ∈ Line.of i j h

theorem line_eq_of {α : Type u_1} [Field α] (i : α × α) (j : α × α) (oh : i ≠ j) (l₂ : Line α) (h : i ∈ l₂ ∧ j ∈ l₂) : l₂ = Line.of i j oh

def Line.horiz {α : Type u_1} [Field α] (l : Line α) : Prop

Equations

• Line.horiz l = ((1, 0, 0) ∈ ↑l)

theorem Line.of_horiz_iff {α : Type u_1} [Field α] (x : α × α) (y : α × α) (h : x ≠ y) : Line.horiz (Line.of x y h) ↔ x.2 = y.2

theorem Line.horiz_constant {α : Type u_1} [Field α] [DecidableEq α] (l : Line α) (x : α × α) (y : α × α) (h : x ∈ l) (h₂ : y ∈ l) (hor : Line.horiz l) : x.2 = y.2

def Line.vert {α : Type u_1} [Field α] (l : Line α) : Prop

Equations

• Line.vert l = ((0, 1, 0) ∈ ↑l)

theorem Line.of_vert_iff {α : Type u_1} [Field α] (x : α × α) (y : α × α) (h : x ≠ y) : Line.vert (Line.of x y h) ↔ x.1 = y.1

theorem Line.vert_constant {α : Type u_1} [Field α] [DecidableEq α] (l : Line α) (x : α × α) (y : α × α) (h : x ∈ l) (h₂ : y ∈ l) (hor : Line.vert l) : x.1 = y.1

def Line.of_equation {α : Type u_1} [Field α] (a : α) (b : α) : Line α

Equations

• Line.of_equation a b = Line.of (0, b) (1, a + b) ⋯

theorem mem_of_equation_iff {α : Type u_1} [Field α] (a : α) (b : α) (x : α × α) : x ∈ Line.of_equation a b ↔ a * x.1 + b = x.2

theorem Line.uncurry_of_equation_injective {α : Type u_1} [Field α] : Function.Injective (Function.uncurry Line.of_equation)

theorem point_intersect {α : Type u_1} [Field α] [Fintype α] (i : α × α) (j : α × α) (oh : i ≠ j) : (Finset.filter (fun (x : Line α) => i ∈ x ∧ j ∈ x) Finset.univ).card = 1

theorem line_intersect {α : Type u_1} [Field α] [Fintype α] (i : Line α) (j : Line α) (h : i ≠ j) : (Finset.filter (fun (x : α × α) => x ∈ i ∧ x ∈ j) Finset.univ).card ≤ 1

noncomputable def Intersections {α : Type u_1} [Field α] (P : Finset (α × α)) (L : Finset (Line α)) : Finset ((α × α) × Line α)

Equations

• Intersections P L = Finset.filter (fun (x : (α × α) × Line α) => x.1 ∈ x.2) (P ×ˢ L)

noncomputable def IntersectionsP {α : Type u_1} [Field α] (P : Finset (α × α)) (L : Line α) : Finset (α × α)

Equations

• IntersectionsP P L = Finset.filter (fun (x : α × α) => x ∈ L) P

noncomputable def IntersectionsL {α : Type u_1} [Field α] (P : α × α) (L : Finset (Line α)) : Finset (Line α)

Equations

• IntersectionsL P L = Finset.filter (fun (x : Line α) => P ∈ x) L

theorem IntP_subset_of_subset {α : Type u_1} [Field α] {P₁ : Finset (α × α)} {P₂ : Finset (α × α)} {l : Line α} (h : P₁ ⊆ P₂) : IntersectionsP P₁ l ⊆ IntersectionsP P₂ l

@[simp]

theorem Int_empty {α : Type u_1} [Field α] {L : Finset (Line α)} : Intersections ∅ L = ∅

@[simp]

theorem Int2_empty {α : Type u_1} [Field α] {P : Finset (α × α)} : Intersections P ∅ = ∅

theorem IntersectionsP_sum {α : Type u_1} [Field α] (P : Finset (α × α)) (L : Finset (Line α)) : (Intersections P L).card = Finset.sum L fun (y : Line α) => (IntersectionsP P y).card

theorem IntersectionsL_sum {α : Type u_1} [Field α] (P : Finset (α × α)) (L : Finset (Line α)) : (Intersections P L).card = Finset.sum P fun (y : α × α) => (IntersectionsL y L).card

theorem lin_ST {α : Type u_1} [Field α] (P : Finset (α × α)) (L : Finset (Line α)) : (Intersections P L).card ≤ P.card * L.card

theorem CS_UB {α : Type u_1} [Field α] [Fintype α] (P : Finset (α × α)) (L : Finset (Line α)) : (Intersections P L).card ^ 2 ≤ L.card * P.card * (L.card + P.card)