data.list.cycle - scilib docs

source

def list.next_or {α : Type u_1} [decidable_eq α] (xs : list α) (x default : α) :

α

Return the z such that x :: z :: _ appears in xs, or default if there is no such z.

Equations

(y :: z :: xs).next_or x default = ite (x = y) z ((z :: xs).next_or x default)
[y].next_or x default = default
list.nil.next_or x default = default

source

@[simp]

theorem list.next_or_nil {α : Type u_1} [decidable_eq α] (x d : α) :

list.nil.next_or x d = d

source

@[simp]

theorem list.next_or_singleton {α : Type u_1} [decidable_eq α] (x y d : α) :

[y].next_or x d = d

source

@[simp]

theorem list.next_or_self_cons_cons {α : Type u_1} [decidable_eq α] (xs : list α) (x y d : α) :

(x :: y :: xs).next_or x d = y

source

theorem list.next_or_cons_of_ne {α : Type u_1} [decidable_eq α] (xs : list α) (y x d : α) (h : x ≠ y) :

(y :: xs).next_or x d = xs.next_or x d

source

theorem list.next_or_eq_next_or_of_mem_of_ne {α : Type u_1} [decidable_eq α] (xs : list α) (x d d' : α) (x_mem : x ∈ xs) (x_ne : x ≠ xs.last _) :

xs.next_or x d = xs.next_or x d'

next_or does not depend on the default value, if the next value appears.

source

theorem list.mem_of_next_or_ne {α : Type u_1} [decidable_eq α] {xs : list α} {x d : α} (h : xs.next_or x d ≠ d) :

x ∈ xs

source

theorem list.next_or_concat {α : Type u_1} [decidable_eq α] {xs : list α} {x : α} (d : α) (h : x ∉ xs) :

(xs ++ [x]).next_or x d = d

source

theorem list.next_or_mem {α : Type u_1} [decidable_eq α] {xs : list α} {x d : α} (hd : d ∈ xs) :

xs.next_or x d ∈ xs

source

def list.next {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∈ l) :

α

Given an element x : α of l : list α such that x ∈ l, get the next element of l. This works from head to tail, (including a check for last element) so it will match on first hit, ignoring later duplicates.

For example:

next [1, 2, 3] 2 _ = 3
next [1, 2, 3] 3 _ = 1
next [1, 2, 3, 2, 4] 2 _ = 3
next [1, 2, 3, 2] 2 _ = 3
next [1, 1, 2, 3, 2] 1 _ = 1

Equations

l.next x h = l.next_or x (l.nth_le 0 _)

source

def list.prev {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∈ l) :

α

Given an element x : α of l : list α such that x ∈ l, get the previous element of l. This works from head to tail, (including a check for last element) so it will match on first hit, ignoring later duplicates.

prev [1, 2, 3] 2 _ = 1
prev [1, 2, 3] 1 _ = 3
prev [1, 2, 3, 2, 4] 2 _ = 1
prev [1, 2, 3, 4, 2] 2 _ = 1
prev [1, 1, 2] 1 _ = 2

Equations

(y :: z :: xs).prev x h = dite (x = y) (λ (hx : x = y), (z :: xs).last _) (λ (hx : ¬x = y), ite (x = z) y ((z :: xs).prev x _))
[y].prev _x _x_1 = y
list.nil.prev _x h = list.prev._main._proof_1.mpr (false.rec α _)

source

@[simp]

theorem list.next_singleton {α : Type u_1} [decidable_eq α] (x y : α) (h : x ∈ [y]) :

[y].next x h = y

source

@[simp]

theorem list.prev_singleton {α : Type u_1} [decidable_eq α] (x y : α) (h : x ∈ [y]) :

[y].prev x h = y

source

theorem list.next_cons_cons_eq' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :

(y :: z :: l).next x h = z

source

@[simp]

theorem list.next_cons_cons_eq {α : Type u_1} [decidable_eq α] (l : list α) (x z : α) (h : x ∈ x :: z :: l) :

(x :: z :: l).next x h = z

source

theorem list.next_ne_head_ne_last {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x ∈ y :: l) (hy : x ≠ y) (hx : x ≠ (y :: l).last _) :

(y :: l).next x h = l.next x _

source

theorem list.next_cons_concat {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (hy : x ≠ y) (hx : x ∉ l) (h : x ∈ y :: l ++ [x] := _) :

(y :: l ++ [x]).next x h = y

source

theorem list.next_last_cons {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x ∈ y :: l) (hy : x ≠ y) (hx : x = (y :: l).last _) (hl : l.nodup) :

(y :: l).next x h = y

source

theorem list.prev_last_cons' {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x ∈ y :: l) (hx : x = y) :

(y :: l).prev x h = (y :: l).last _

source

@[simp]

theorem list.prev_last_cons {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∈ x :: l) :

(x :: l).prev x h = (x :: l).last _

source

theorem list.prev_cons_cons_eq' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :

(y :: z :: l).prev x h = (z :: l).last _

source

@[simp]

theorem list.prev_cons_cons_eq {α : Type u_1} [decidable_eq α] (l : list α) (x z : α) (h : x ∈ x :: z :: l) :

(x :: z :: l).prev x h = (z :: l).last _

source

theorem list.prev_cons_cons_of_ne' {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) :

(y :: z :: l).prev x h = y

source

theorem list.prev_cons_cons_of_ne {α : Type u_1} [decidable_eq α] (l : list α) (x y : α) (h : x ∈ y :: x :: l) (hy : x ≠ y) :

(y :: x :: l).prev x h = y

source

theorem list.prev_ne_cons_cons {α : Type u_1} [decidable_eq α] (l : list α) (x y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x ≠ z) :

(y :: z :: l).prev x h = (z :: l).prev x _

source

theorem list.next_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∈ l) :

l.next x h ∈ l

source

theorem list.prev_mem {α : Type u_1} [decidable_eq α] (l : list α) (x : α) (h : x ∈ l) :

l.prev x h ∈ l

source

theorem list.next_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ℕ) (hn : n < l.length) :

l.next (l.nth_le n hn) _ = l.nth_le ((n + 1) % l.length) _

source

theorem list.prev_nth_le {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (n : ℕ) (hn : n < l.length) :

l.prev (l.nth_le n hn) _ = l.nth_le ((n + (l.length - 1)) % l.length) _

source

theorem list.pmap_next_eq_rotate_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :

list.pmap l.next l _ = l.rotate 1

source

theorem list.pmap_prev_eq_rotate_length_sub_one {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) :

list.pmap l.prev l _ = l.rotate (l.length - 1)

source

theorem list.prev_next {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x ∈ l) :

l.prev (l.next x hx) _ = x

source

theorem list.next_prev {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x ∈ l) :

l.next (l.prev x hx) _ = x

source

theorem list.prev_reverse_eq_next {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x ∈ l) :

l.reverse.prev x _ = l.next x hx

source

theorem list.next_reverse_eq_prev {α : Type u_1} [decidable_eq α] (l : list α) (h : l.nodup) (x : α) (hx : x ∈ l) :

l.reverse.next x _ = l.prev x hx

source

theorem list.is_rotated_next_eq {α : Type u_1} [decidable_eq α] {l l' : list α} (h : l ~r l') (hn : l.nodup) {x : α} (hx : x ∈ l) :

l.next x hx = l'.next x _

source

theorem list.is_rotated_prev_eq {α : Type u_1} [decidable_eq α] {l l' : list α} (h : l ~r l') (hn : l.nodup) {x : α} (hx : x ∈ l) :

l.prev x hx = l'.prev x _

source

def cycle (α : Type u_1) :

Type u_1

cycle α is the quotient of list α by cyclic permutation. Duplicates are allowed.

Equations

cycle α = quotient (list.is_rotated.setoid α)

Instances for cycle

source

@[protected, instance]

def cycle.has_coe {α : Type u_1} :

has_coe (list α) (cycle α)

Equations

cycle.has_coe = {coe := quot.mk setoid.r}

source

@[simp]

theorem cycle.coe_eq_coe {α : Type u_1} {l₁ l₂ : list α} :

↑l₁ = ↑l₂ ↔ l₁ ~r l₂

source

@[simp]

theorem cycle.mk_eq_coe {α : Type u_1} (l : list α) :

quot.mk setoid.r l = ↑l

source

@[simp]

theorem cycle.mk'_eq_coe {α : Type u_1} (l : list α) :

quotient.mk' l = ↑l

source

theorem cycle.coe_cons_eq_coe_append {α : Type u_1} (l : list α) (a : α) :

↑(a :: l) = ↑(l ++ [a])

source

def cycle.nil {α : Type u_1} :

cycle α

The unique empty cycle.

Equations

cycle.nil = ↑list.nil

source

@[simp]

theorem cycle.coe_nil {α : Type u_1} :

↑list.nil = cycle.nil

source

@[simp]

theorem cycle.coe_eq_nil {α : Type u_1} (l : list α) :

↑l = cycle.nil ↔ l = list.nil

source

@[protected, instance]

def cycle.has_emptyc {α : Type u_1} :

has_emptyc (cycle α)

For consistency with list.has_emptyc.

Equations

cycle.has_emptyc = {emptyc := cycle.nil α}

source

@[simp]

theorem cycle.empty_eq {α : Type u_1} :

∅ = cycle.nil

source

@[protected, instance]

def cycle.inhabited {α : Type u_1} :

inhabited (cycle α)

Equations

cycle.inhabited = {default := cycle.nil α}

source

theorem cycle.induction_on {α : Type u_1} {C : cycle α → Prop} (s : cycle α) (H0 : C cycle.nil) (HI : ∀ (a : α) (l : list α), C ↑l → C ↑(a :: l)) :

C s

An induction principle for cycle. Use as induction s using cycle.induction_on.

source

def cycle.mem {α : Type u_1} (a : α) (s : cycle α) :

Prop

For x : α, s : cycle α, x ∈ s indicates that x occurs at least once in s.

Equations

cycle.mem a s = quot.lift_on s (λ (l : list α), a ∈ l) _

source

@[protected, instance]

def cycle.has_mem {α : Type u_1} :

has_mem α (cycle α)

Equations

cycle.has_mem = {mem := cycle.mem α}

source

@[simp]

theorem cycle.mem_coe_iff {α : Type u_1} {a : α} {l : list α} :

a ∈ ↑l ↔ a ∈ l

source

@[simp]

theorem cycle.not_mem_nil {α : Type u_1} (a : α) :

a ∉ cycle.nil

source

@[protected, instance]

def cycle.decidable_eq {α : Type u_1} [decidable_eq α] :

decidable_eq (cycle α)

Equations

cycle.decidable_eq = λ (s₁ s₂ : cycle α), quotient.rec_on_subsingleton₂' s₁ s₂ (λ (l₁ l₂ : list α), decidable_of_iff' (setoid.r l₁ l₂) _)

source

@[protected, instance]

def cycle.has_mem.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (s : cycle α) :

decidable (x ∈ s)

Equations

cycle.has_mem.mem.decidable x s = quotient.rec_on_subsingleton' s (λ (l : list α), list.decidable_mem x l)

source

def cycle.reverse {α : Type u_1} (s : cycle α) :

cycle α

Reverse a s : cycle α by reversing the underlying list.

Equations

s.reverse = quot.map list.reverse cycle.reverse._proof_1 s

source

@[simp]

theorem cycle.reverse_coe {α : Type u_1} (l : list α) :

↑l.reverse = ↑(l.reverse)

source

@[simp]

theorem cycle.mem_reverse_iff {α : Type u_1} {a : α} {s : cycle α} :

a ∈ s.reverse ↔ a ∈ s

source

@[simp]

theorem cycle.reverse_reverse {α : Type u_1} (s : cycle α) :

s.reverse.reverse = s

source

@[simp]

theorem cycle.reverse_nil {α : Type u_1} :

cycle.nil.reverse = cycle.nil

source

def cycle.length {α : Type u_1} (s : cycle α) :

ℕ

The length of the s : cycle α, which is the number of elements, counting duplicates.

Equations

s.length = quot.lift_on s list.length cycle.length._proof_1

source

@[simp]

theorem cycle.length_coe {α : Type u_1} (l : list α) :

↑l.length = l.length

source

@[simp]

theorem cycle.length_nil {α : Type u_1} :

cycle.nil.length = 0

source

@[simp]

theorem cycle.length_reverse {α : Type u_1} (s : cycle α) :

s.reverse.length = s.length

source

def cycle.subsingleton {α : Type u_1} (s : cycle α) :

Prop

A s : cycle α that is at most one element.

Equations

s.subsingleton = (s.length ≤ 1)

source

theorem cycle.subsingleton_nil {α : Type u_1} :

cycle.nil.subsingleton

source

theorem cycle.length_subsingleton_iff {α : Type u_1} {s : cycle α} :

s.subsingleton ↔ s.length ≤ 1

source

@[simp]

theorem cycle.subsingleton_reverse_iff {α : Type u_1} {s : cycle α} :

s.reverse.subsingleton ↔ s.subsingleton

source

theorem cycle.subsingleton.congr {α : Type u_1} {s : cycle α} (h : s.subsingleton) ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) :

x = y

source

def cycle.nontrivial {α : Type u_1} (s : cycle α) :

Prop

A s : cycle α that is made up of at least two unique elements.

Equations

s.nontrivial = ∃ (x y : α) (h : x ≠ y), x ∈ s ∧ y ∈ s

Instances for cycle.nontrivial

cycle.nontrivial.decidable

source

@[simp]

theorem cycle.nontrivial_coe_nodup_iff {α : Type u_1} {l : list α} (hl : l.nodup) :

↑l.nontrivial ↔ 2 ≤ l.length

source

@[simp]

theorem cycle.nontrivial_reverse_iff {α : Type u_1} {s : cycle α} :

s.reverse.nontrivial ↔ s.nontrivial

source

theorem cycle.length_nontrivial {α : Type u_1} {s : cycle α} (h : s.nontrivial) :

2 ≤ s.length

source

def cycle.nodup {α : Type u_1} (s : cycle α) :

Prop

The s : cycle α contains no duplicates.

Equations

s.nodup = quot.lift_on s list.nodup cycle.nodup._proof_1

Instances for cycle.nodup

cycle.nodup.decidable

source

@[simp]

theorem cycle.nodup_nil {α : Type u_1} :

cycle.nil.nodup

source

@[simp]

theorem cycle.nodup_coe_iff {α : Type u_1} {l : list α} :

↑l.nodup ↔ l.nodup

source

@[simp]

theorem cycle.nodup_reverse_iff {α : Type u_1} {s : cycle α} :

s.reverse.nodup ↔ s.nodup

source

theorem cycle.subsingleton.nodup {α : Type u_1} {s : cycle α} (h : s.subsingleton) :

s.nodup

source

theorem cycle.nodup.nontrivial_iff {α : Type u_1} {s : cycle α} (h : s.nodup) :

s.nontrivial ↔ ¬s.subsingleton

source

def cycle.to_multiset {α : Type u_1} (s : cycle α) :

multiset α

The s : cycle α as a multiset α.

Equations

s.to_multiset = quotient.lift_on' s coe cycle.to_multiset._proof_1

source

@[simp]

theorem cycle.coe_to_multiset {α : Type u_1} (l : list α) :

↑l.to_multiset = ↑l

source

@[simp]

theorem cycle.nil_to_multiset {α : Type u_1} :

cycle.nil.to_multiset = 0

source

@[simp]

theorem cycle.card_to_multiset {α : Type u_1} (s : cycle α) :

⇑multiset.card s.to_multiset = s.length

source

@[simp]

theorem cycle.to_multiset_eq_nil {α : Type u_1} {s : cycle α} :

s.to_multiset = 0 ↔ s = cycle.nil

source

def cycle.map {α : Type u_1} {β : Type u_2} (f : α → β) :

cycle α → cycle β

The lift of list.map.

Equations

cycle.map f = quotient.map' (list.map f) _

source

@[simp]

theorem cycle.map_nil {α : Type u_1} {β : Type u_2} (f : α → β) :

cycle.map f cycle.nil = cycle.nil

source

@[simp]

theorem cycle.map_coe {α : Type u_1} {β : Type u_2} (f : α → β) (l : list α) :

cycle.map f ↑l = ↑(list.map f l)

source

@[simp]

theorem cycle.map_eq_nil {α : Type u_1} {β : Type u_2} (f : α → β) (s : cycle α) :

cycle.map f s = cycle.nil ↔ s = cycle.nil

source

@[simp]

theorem cycle.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : cycle α} :

b ∈ cycle.map f s ↔ ∃ (a : α), a ∈ s ∧ f a = b

source

def cycle.lists {α : Type u_1} (s : cycle α) :

multiset (list α)

The multiset of lists that can make the cycle.

Equations

s.lists = quotient.lift_on' s (λ (l : list α), ↑(l.cyclic_permutations)) cycle.lists._proof_1

source

@[simp]

theorem cycle.lists_coe {α : Type u_1} (l : list α) :

↑l.lists = ↑(l.cyclic_permutations)

source

@[simp]

theorem cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : cycle α} {l : list α} :

l ∈ s.lists ↔ ↑l = s

source

@[simp]

theorem cycle.lists_nil {α : Type u_1} :

cycle.nil.lists = ↑[list.nil]

source

def cycle.decidable_nontrivial_coe {α : Type u_1} [decidable_eq α] (l : list α) :

decidable ↑l.nontrivial

Auxiliary decidability algorithm for lists that contain at least two unique elements.

Equations

cycle.decidable_nontrivial_coe (x :: y :: l) = dite (x = y) (λ (h : x = y), decidable_of_iff' ↑(x :: l).nontrivial _) (λ (h : ¬x = y), decidable.is_true _)
cycle.decidable_nontrivial_coe [x] = decidable.is_false _
cycle.decidable_nontrivial_coe list.nil = decidable.is_false cycle.decidable_nontrivial_coe._main._pack._proof_1

source

@[protected, instance]

def cycle.nontrivial.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :

decidable s.nontrivial

Equations

cycle.nontrivial.decidable = quot.rec_on_subsingleton s cycle.decidable_nontrivial_coe

source

@[protected, instance]

def cycle.nodup.decidable {α : Type u_1} [decidable_eq α] {s : cycle α} :

decidable s.nodup

Equations

cycle.nodup.decidable = quot.rec_on_subsingleton s list.nodup_decidable

source

@[protected, instance]

def cycle.fintype_nodup_cycle {α : Type u_1} [decidable_eq α] [fintype α] :

fintype {s // s.nodup}

Equations

cycle.fintype_nodup_cycle = fintype.of_surjective (λ (l : {l // l.nodup}), ⟨↑(l.val), _⟩) cycle.fintype_nodup_cycle._proof_2

source

@[protected, instance]

def cycle.fintype_nodup_nontrivial_cycle {α : Type u_1} [decidable_eq α] [fintype α] :

fintype {s // s.nodup ∧ s.nontrivial}

Equations

cycle.fintype_nodup_nontrivial_cycle = fintype.subtype (finset.filter cycle.nontrivial (finset.map (function.embedding.subtype (λ (s : cycle α), s.nodup)) finset.univ)) cycle.fintype_nodup_nontrivial_cycle._proof_1

source

def cycle.to_finset {α : Type u_1} [decidable_eq α] (s : cycle α) :

finset α

The s : cycle α as a finset α.

Equations

s.to_finset = s.to_multiset.to_finset

source

@[simp]

theorem cycle.to_finset_to_multiset {α : Type u_1} [decidable_eq α] (s : cycle α) :

s.to_multiset.to_finset = s.to_finset

source

@[simp]

theorem cycle.coe_to_finset {α : Type u_1} [decidable_eq α] (l : list α) :

↑l.to_finset = l.to_finset

source

@[simp]

theorem cycle.nil_to_finset {α : Type u_1} [decidable_eq α] :

cycle.nil.to_finset = ∅

source

@[simp]

theorem cycle.to_finset_eq_nil {α : Type u_1} [decidable_eq α] {s : cycle α} :

s.to_finset = ∅ ↔ s = cycle.nil

source

def cycle.next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

α

Given a s : cycle α such that nodup s, retrieve the next element after x ∈ s.

Equations

cycle.next = λ (s : cycle α), quot.hrec_on s (λ (l : list α) (hn : cycle.nodup (quot.mk setoid.r l)) (x : α) (hx : x ∈ quot.mk setoid.r l), l.next x hx) cycle.next._proof_1

source

def cycle.prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

α

Given a s : cycle α such that nodup s, retrieve the previous element before x ∈ s.

Equations

cycle.prev = λ (s : cycle α), quot.hrec_on s (λ (l : list α) (hn : cycle.nodup (quot.mk setoid.r l)) (x : α) (hx : x ∈ quot.mk setoid.r l), l.prev x hx) cycle.prev._proof_1

source

@[simp]

theorem cycle.prev_reverse_eq_next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.reverse.prev _ x _ = s.next hs x hx

source

@[simp]

theorem cycle.next_reverse_eq_prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.reverse.next _ x _ = s.prev hs x hx

source

@[simp]

theorem cycle.next_mem {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.next hs x hx ∈ s

source

theorem cycle.prev_mem {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.prev hs x hx ∈ s

source

@[simp]

theorem cycle.prev_next {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.prev hs (s.next hs x hx) _ = x

source

@[simp]

theorem cycle.next_prev {α : Type u_1} [decidable_eq α] (s : cycle α) (hs : s.nodup) (x : α) (hx : x ∈ s) :

s.next hs (s.prev hs x hx) _ = x

source

@[protected, instance]

meta def cycle.has_repr {α : Type u_1} [has_repr α] :

has_repr (cycle α)

We define a representation of concrete cycles, available when viewing them in a goal state or via #eval, when over representable types. For example, the cycle (2 1 4 3) will be shown as c[2, 1, 4, 3]. Two equal cycles may be printed differently if their internal representation is different.

source

def cycle.chain {α : Type u_1} (r : α → α → Prop) (c : cycle α) :

Prop

chain R s means that R holds between adjacent elements of s.

chain R ([a, b, c] : cycle α) ↔ R a b ∧ R b c ∧ R c a

Equations

cycle.chain r c = quotient.lift_on' c (λ (l : list α), cycle.chain._match_1 r l) _
cycle.chain._match_1 r (a :: m) = list.chain r a (m ++ [a])
cycle.chain._match_1 r list.nil = true

source

@[simp]

theorem cycle.chain.nil {α : Type u_1} (r : α → α → Prop) :

cycle.chain r cycle.nil

source

@[simp]

theorem cycle.chain_coe_cons {α : Type u_1} (r : α → α → Prop) (a : α) (l : list α) :

cycle.chain r ↑(a :: l) ↔ list.chain r a (l ++ [a])

source

@[simp]

theorem cycle.chain_singleton {α : Type u_1} (r : α → α → Prop) (a : α) :

cycle.chain r ↑[a] ↔ r a a

source

theorem cycle.chain_ne_nil {α : Type u_1} (r : α → α → Prop) {l : list α} (hl : l ≠ list.nil) :

cycle.chain r ↑l ↔ list.chain r (l.last hl) l

source

theorem cycle.chain_map {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (f : β → α) {s : cycle β} :

cycle.chain r (cycle.map f s) ↔ cycle.chain (λ (a b : β), r (f a) (f b)) s

source

theorem cycle.chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :

cycle.chain r ↑(list.range n.succ) ↔ r n 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

source

theorem cycle.chain.imp {α : Type u_1} {s : cycle α} {r₁ r₂ : α → α → Prop} (H : ∀ (a b : α), r₁ a b → r₂ a b) (p : cycle.chain r₁ s) :

cycle.chain r₂ s

source

theorem cycle.chain_mono {α : Type u_1} :

monotone cycle.chain

As a function from a relation to a predicate, chain is monotonic.

source

theorem cycle.chain_of_pairwise {α : Type u_1} {r : α → α → Prop} {s : cycle α} :

(∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b) → cycle.chain r s

source

theorem cycle.chain_iff_pairwise {α : Type u_1} {r : α → α → Prop} {s : cycle α} [is_trans α r] :

cycle.chain r s ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b

source

theorem cycle.chain.eq_nil_of_irrefl {α : Type u_1} {r : α → α → Prop} {s : cycle α} [is_trans α r] [is_irrefl α r] (h : cycle.chain r s) :

s = cycle.nil

source

theorem cycle.chain.eq_nil_of_well_founded {α : Type u_1} {r : α → α → Prop} {s : cycle α} [is_well_founded α r] (h : cycle.chain r s) :

s = cycle.nil

source

theorem cycle.forall_eq_of_chain {α : Type u_1} {r : α → α → Prop} {s : cycle α} [is_trans α r] [is_antisymm α r] (hs : cycle.chain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :

a = b

scilib documentation

Cycles of a list #