structure AP.FSP : Type

• get : ℕ → Set PointZ

theorem AP.FSP.ext_iff {x y : FSP} : x = y ↔ x.get = y.get

theorem AP.FSP.ext {x y : FSP} (get : x.get = y.get) : x = y

@[instance_reducible]

instance AP.FSP.instEmptyCollection : EmptyCollection FSP

Equations

• AP.FSP.instEmptyCollection = { emptyCollection := { get := fun (x : ℕ) => ∅ } }

theorem AP.FSP.empty_def : ∅ = { get := fun (x : ℕ) => ∅ }

@[instance_reducible]

instance AP.FSP.instInhabited : Inhabited FSP

Equations

• AP.FSP.instInhabited = { default := ∅ }

theorem AP.FSP.default_def : default = ∅

@[instance_reducible]

instance AP.FSP.instUnion : Union FSP

Equations

• AP.FSP.instUnion = { union := fun (a b : AP.FSP) => { get := fun (i : ℕ) => a.get i ∪ b.get i } }

theorem AP.FSP.union_def {a b : FSP} : a ∪ b = { get := fun (i : ℕ) => a.get i ∪ b.get i }

@[instance_reducible]

instance AP.FSP.instInter : Inter FSP

Equations

• AP.FSP.instInter = { inter := fun (a b : AP.FSP) => { get := fun (i : ℕ) => a.get i ∩ b.get i } }

theorem AP.FSP.inter_def {a b : FSP} : a ∩ b = { get := fun (i : ℕ) => a.get i ∩ b.get i }

def AP.FSP.next (fsp : FSP) : FSP

Equations

• fsp.next = { get := fun (i : ℕ) => match i with | 0 => fsp.get 0 ∪ fsp.get 1 | n.succ => fsp.get (n + 2) }

def AP.FSP.offset (fsp : FSP) (n : ℕ) : FSP

Equations

• fsp.offset n = AP.FSP.next^[n] fsp

def AP.FSP.hasLe (a : FSP) (n : ℕ) (p : PointZ) : Prop

Equations

• a.hasLe n p = ∃ k ≤ n, p ∈ a.get k

def AP.FSP.insertSet (fsp : FSP) (n : ℕ) (ps : Set PointZ) : FSP

Equations

• fsp.insertSet n ps = { get := fun (i : ℕ) => if i = n then ps ∪ fsp.get i else fsp.get i }

def AP.FSP.insert (fsp : FSP) (n : ℕ) (p : PointZ) : FSP

Equations

• fsp.insert n p = fsp.insertSet n {p}

def AP.FSP.Subset (a b : FSP) : Prop

Equations

• a.Subset b = ∀ ⦃i : ℕ⦄, a.get i ⊆ b.get i

@[instance_reducible]

instance AP.FSP.instHasSubset : HasSubset FSP

Equations

• AP.FSP.instHasSubset = { Subset := AP.FSP.Subset }

@[simp]

theorem AP.FSP.hasLe_next {a : FSP} {n : ℕ} {p : PointZ} : a.next.hasLe n p ↔ a.hasLe (n + 1) p

theorem AP.FSP.hasLe_insertSet_eq_of_lt {fsp : FSP} {n k : ℕ} {ps : Set PointZ} (h : k < n) : (fsp.insertSet n ps).hasLe k = fsp.hasLe k

theorem AP.FSP.hasLe_insert_eq_of_lt {fsp : FSP} {n k : ℕ} {p : PointZ} (h : k < n) : (fsp.insert n p).hasLe k = fsp.hasLe k

@[simp]

theorem AP.FSP.insertSet_empty {fsp : FSP} {n : ℕ} : fsp.insertSet n ∅ = fsp

theorem AP.FSP.insertSet_insert {fsp : FSP} {n : ℕ} {p : PointZ} {ps : Set PointZ} : (fsp.insertSet n ps).insert n p = fsp.insertSet n (insert p ps)

theorem AP.FSP.insertSet_set_insert {fsp : FSP} {n : ℕ} {p : PointZ} {ps : Set PointZ} : fsp.insertSet n (insert p ps) = (fsp.insertSet n ps).insert n p

@[simp]

theorem AP.FSP.get_insertSet_of_eq {fsp : FSP} {n : ℕ} {ps : Set PointZ} : (fsp.insertSet n ps).get n = ps ∪ fsp.get n

@[simp]

theorem AP.FSP.get_insert_of_eq {fsp : FSP} {n : ℕ} {p : PointZ} : (fsp.insert n p).get n = insert p (fsp.get n)

theorem AP.FSP.hasLe_insertSet_of_le {fsp : FSP} {m n k : ℕ} {ps : Set PointZ} {p : PointZ} (h₁ : (fsp.insertSet m ps).hasLe k p) (h₂ : m ≤ k) (h₃ : n ≤ k) : (fsp.insertSet n ps).hasLe k p

theorem AP.FSP.hasLe_insert_of_le {fsp : FSP} {m n k : ℕ} {p p₁ : PointZ} (h₁ : (fsp.insert m p).hasLe k p₁) (h₂ : m ≤ k) (h₃ : n ≤ k) : (fsp.insert n p).hasLe k p₁

theorem AP.FSP.insertSet_comm {fsp : FSP} {n m : ℕ} {ps₁ ps₂ : Set PointZ} : (fsp.insertSet n ps₁).insertSet m ps₂ = (fsp.insertSet m ps₂).insertSet n ps₁

theorem AP.FSP.insert_comm {fsp : FSP} {n m : ℕ} {p₁ p₂ : PointZ} : (fsp.insert n p₁).insert m p₂ = (fsp.insert m p₂).insert n p₁

theorem AP.FSP.insertSet_insert_comm {fsp : FSP} {n m : ℕ} {ps₁ : Set PointZ} {p₂ : PointZ} : (fsp.insertSet n ps₁).insert m p₂ = (fsp.insert m p₂).insertSet n ps₁

theorem AP.FSP.insert_insertSet_comm {fsp : FSP} {n m : ℕ} {p₁ : PointZ} {ps₂ : Set PointZ} : (fsp.insert n p₁).insertSet m ps₂ = (fsp.insertSet m ps₂).insert n p₁

theorem AP.FSP.hasLe_insertSet_of_hasLe {fsp : FSP} {n k : ℕ} {ps : Set PointZ} {p : PointZ} (h₁ : fsp.hasLe k p) : (fsp.insertSet n ps).hasLe k p

theorem AP.FSP.hasLe_insertSet_of_le_and_le {fsp : FSP} {m n k : ℕ} {ps : Set PointZ} {p : PointZ} (h₁ : (fsp.insertSet n ps).hasLe k p) (h₂ : m ≤ n) : (fsp.insertSet m ps).hasLe k p

theorem AP.FSP.hasLe_insert_of_le_and_le {fsp : FSP} {m n k : ℕ} {p p₁ : PointZ} (h₁ : (fsp.insert n p).hasLe k p₁) (h₂ : m ≤ n) : (fsp.insert m p).hasLe k p₁

@[simp]

theorem AP.FSP.get_insertSet_of_ne {fsp : FSP} {n k : ℕ} {ps : Set PointZ} (h : k ≠ n) : (fsp.insertSet n ps).get k = fsp.get k

@[simp]

theorem AP.FSP.get_insert_of_ne {fsp : FSP} {n k : ℕ} {p : PointZ} (h : k ≠ n) : (fsp.insert n p).get k = fsp.get k

theorem AP.FSP.insert_eq_of_mem {fsp : FSP} {n : ℕ} {p : PointZ} (h : p ∈ fsp.get n) : fsp.insert n p = fsp

@[simp]

theorem AP.FSP.offset_zero {fsp : FSP} : fsp.offset 0 = fsp

@[simp]

theorem AP.FSP.offset_one {fsp : FSP} : fsp.offset 1 = fsp.next

theorem AP.FSP.offset_succ {fsp : FSP} {n : ℕ} : fsp.offset (n + 1) = fsp.next.offset n

theorem AP.FSP.offset_succ' {fsp : FSP} {n : ℕ} : fsp.offset (n + 1) = (fsp.offset n).next

@[simp]

theorem AP.FSP.mem_get_zero_next_iff {fsp : FSP} {p : PointZ} : p ∈ fsp.next.get 0 ↔ p ∈ fsp.get 0 ∨ p ∈ fsp.get 1

@[simp]

theorem AP.FSP.mem_get_zero_offset_iff {fsp : FSP} {n : ℕ} {p : PointZ} : p ∈ (fsp.offset n).get 0 ↔ ∃ k ≤ n, p ∈ fsp.get k

@[simp]

theorem AP.FSP.hasLe_offset {fsp : FSP} {n k : ℕ} {p : PointZ} : (fsp.offset n).hasLe k p ↔ fsp.hasLe (k + n) p

theorem AP.FSP.hasLe_of_le {fsp : FSP} {n k : ℕ} {p : PointZ} (h₁ : fsp.hasLe k p) (h₂ : k ≤ n) : fsp.hasLe n p

theorem AP.FSP.hasLe_of_add_left {fsp : FSP} {n k : ℕ} {p : PointZ} (h : fsp.hasLe n p) : fsp.hasLe (k + n) p

theorem AP.FSP.hasLe_of_add_right {fsp : FSP} {n k : ℕ} {p : PointZ} (h : fsp.hasLe n p) : fsp.hasLe (n + k) p

@[simp]

theorem AP.FSP.hasLe_zero {fsp : FSP} {p : PointZ} : fsp.hasLe 0 p ↔ p ∈ fsp.get 0

theorem AP.FSP.next_offset {fsp : FSP} {n : ℕ} : (fsp.offset n).next = fsp.offset (n + 1)

theorem AP.FSP.next_insertSet_succ {fsp : FSP} {n : ℕ} {set : Set PointZ} : (fsp.insertSet (n + 1) set).next = fsp.next.insertSet n set

theorem AP.FSP.next_insert_succ {fsp : FSP} {n : ℕ} {p : PointZ} : (fsp.insert (n + 1) p).next = fsp.next.insert n p

@[simp]

theorem AP.FSP.insertSet_idem {fsp : FSP} {n : ℕ} {set : Set PointZ} : (fsp.insertSet n set).insertSet n set = fsp.insertSet n set

@[simp]

theorem AP.FSP.insert_idem {fsp : FSP} {n : ℕ} {p : PointZ} : (fsp.insert n p).insert n p = fsp.insert n p

@[simp]

theorem AP.FSP.mem_get_succ_offset_iff {fsp : FSP} {n k : ℕ} {p : PointZ} : p ∈ (fsp.offset n).get (k + 1) ↔ p ∈ fsp.get (n + k + 1)

@[simp]

theorem AP.FSP.get_empty : ∅.get = fun (x : ℕ) => ∅

@[simp]

theorem AP.FSP.hasLe_empty : ∅.hasLe = fun (x : ℕ) (x_1 : PointZ) => False

theorem AP.FSP.subset_def {a b : FSP} : a ⊆ b ↔ ∀ ⦃i : ℕ⦄, a.get i ⊆ b.get i

@[simp]

theorem AP.FSP.get_union {a b : FSP} {i : ℕ} : (a ∪ b).get i = a.get i ∪ b.get i

@[simp]

theorem AP.FSP.hasLe_union {a b : FSP} {i : ℕ} {p : PointZ} : (a ∪ b).hasLe i p ↔ a.hasLe i p ∨ b.hasLe i p

theorem AP.FSP.insert_union {a b : FSP} {i : ℕ} {p : PointZ} : (a ∪ b).insert i p = a.insert i p ∪ b.insert i p

@[simp]

theorem AP.FSP.union_empty {a : FSP} : a ∪ ∅ = a

@[simp]

theorem AP.FSP.union_insertSet {a b : FSP} {i : ℕ} {ps : Set PointZ} : a ∪ b.insertSet i ps = (a ∪ b).insertSet i ps

theorem AP.FSP.hasLe_succ {a : FSP} {i : ℕ} {p : PointZ} : a.hasLe (i + 1) p ↔ a.hasLe i p ∨ p ∈ a.get (i + 1)

theorem AP.FSP.get_offset {a : FSP} {n i : ℕ} : (a.offset n).get i = if i = 0 then {p : PointZ | a.hasLe n p} else a.get (n + i)