BipartiteLink.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.four_le_link line 18
Source documentation
A cyclic link whose steps alternate bipartition, with no two-step backtrack, has at least four actual corners. This is a cardinality result about the permutation orbit, not a simple-cycle field supplied by a user.
```
lemma four_le_link (p : Perm D) (a : D) (c : D → Bool)
    (hc : ∀ x, p.SameCycle a x → c (p x) ≠ c x)
    (h₂ : p (p a) ≠ a) : 4 ≤ Fintype.card {x // p.SameCycle a x} := by
…
```