Complex shapes with no loop

Let c : ComplexShape ι. We define a type class c.HasNoLoop which expresses that ¬ c.Rel i i for all i : ι.

class ComplexShape.HasNoLoop {ι : Type u_1} (c : ComplexShape ι) : Prop

The condition that c.Rel i i does not hold for any i.

• not_rel_self (i : ι) : ¬c.Rel i i

theorem ComplexShape.not_rel_self {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι) : ¬c.Rel j j

theorem ComplexShape.not_rel_of_eq {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] {j j' : ι} (h : j = j') : ¬c.Rel j j'

instance ComplexShape.instHasNoLoopSymm {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] : c.symm.HasNoLoop

theorem ComplexShape.exists_distinct_prev_or {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι) : (∃ (k : ι), c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

theorem ComplexShape.exists_distinct_next_or {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι) : (∃ (i : ι), c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

theorem ComplexShape.hasNoLoop_up' {α : Type u_2} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] (a : α) (ha : a ≠ 0) : (up' a).HasNoLoop

theorem ComplexShape.hasNoLoop_down' {α : Type u_2} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] (a : α) (ha : a ≠ 0) : (down' a).HasNoLoop

theorem ComplexShape.hasNoLoop_up {α : Type u_2} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] [One α] (ha : 1 ≠ 0) : (up α).HasNoLoop

theorem ComplexShape.hasNoLoop_down {α : Type u_2} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] [One α] (ha : 1 ≠ 0) : (down α).HasNoLoop

instance ComplexShape.instHasNoLoopIntUp : (up ℤ).HasNoLoop

instance ComplexShape.instHasNoLoopNatUp : (up ℕ).HasNoLoop

instance ComplexShape.instHasNoLoopIntDown : (down ℤ).HasNoLoop

instance ComplexShape.instHasNoLoopNatDown : (down ℕ).HasNoLoop